Skip to content

Commit 8dbb710

Browse files
authored
feat(Polymorph-CLI)!: refactor CLI arguements (#195)
BREAKING CHANGE: `--output-dafny` now takes a Path, just like `--output-dotnet` and `--output-java`. `--output-local-service-test` is now `--local-service-test` and does NOT take path. Invoking `--output-local-service-test` will cause an error. Invoking `--local-service-test` with a PATH will cause an error. However, to mitigate transition pain, if `--ouput-dafny` is given with no argument, the generated Dafny will be placed in the Model path. Otherwise, Generated Dafny will be written to the value of `--output-dafny`.
1 parent ddf8a51 commit 8dbb710

File tree

4 files changed

+171
-164
lines changed

4 files changed

+171
-164
lines changed

TestModels/SharedMakefile.mk

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -142,29 +142,29 @@ _polymorph_dependencies:
142142
)
143143

144144
# `polymorph_code_gen` is the generate-for-multiple-languages target
145-
polymorph_code_gen: OUTPUT_DAFNY=--output-dafny --include-dafny $(STANDARD_LIBRARY_PATH)/src/Index.dfy
145+
polymorph_code_gen: OUTPUT_DAFNY=--output-dafny $(LIBRARY_ROOT)/Model --include-dafny $(STANDARD_LIBRARY_PATH)/src/Index.dfy
146146
polymorph_code_gen: OUTPUT_DOTNET=--output-dotnet $(LIBRARY_ROOT)/runtimes/net/Generated/
147147
polymorph_code_gen: _polymorph
148148
# Generate wrapped code for all languages that support wrapped services
149149
polymorph_code_gen: OUTPUT_DAFNY_WRAPPED=--output-dafny $(LIBRARY_ROOT)/Model --include-dafny $(STANDARD_LIBRARY_PATH)/src/Index.dfy
150150
polymorph_code_gen: OUTPUT_DOTNET_WRAPPED=--output-dotnet $(LIBRARY_ROOT)/runtimes/net/Generated/Wrapped
151-
polymorph_code_gen: OUTPUT_LOCAL_SERVICE=--output-local-service-test $(LIBRARY_ROOT)/Model
151+
polymorph_code_gen: OUTPUT_LOCAL_SERVICE=--local-service-test
152152
polymorph_code_gen: _polymorph_wrapped
153153
polymorph_code_gen: POLYMORPH_LANGUAGE_TARGET=code_gen
154154
polymorph_code_gen: _polymorph_dependencies
155155

156-
polymorph_dafny: OUTPUT_DAFNY=--output-dafny --include-dafny $(STANDARD_LIBRARY_PATH)/src/Index.dfy
156+
polymorph_dafny: OUTPUT_DAFNY=--output-dafny $(LIBRARY_ROOT)/Model --include-dafny $(STANDARD_LIBRARY_PATH)/src/Index.dfy
157157
polymorph_dafny: _polymorph
158158
polymorph_dafny: OUTPUT_DAFNY_WRAPPED=--output-dafny $(LIBRARY_ROOT)/Model --include-dafny $(STANDARD_LIBRARY_PATH)/src/Index.dfy
159-
polymorph_dafny: OUTPUT_LOCAL_SERVICE=--output-local-service-test $(LIBRARY_ROOT)/Model
159+
polymorph_dafny: OUTPUT_LOCAL_SERVICE=--local-service-test
160160
polymorph_dafny: _polymorph_wrapped
161161
polymorph_dafny: POLYMORPH_LANGUAGE_TARGET=dafny
162162
polymorph_dafny: _polymorph_dependencies
163163

164164
polymorph_net: OUTPUT_DOTNET=--output-dotnet $(LIBRARY_ROOT)/runtimes/net/Generated/
165165
polymorph_net: _polymorph
166166
polymorph_net: OUTPUT_DOTNET_WRAPPED=--output-dotnet $(LIBRARY_ROOT)/runtimes/net/Generated/Wrapped
167-
polymorph_net: OUTPUT_LOCAL_SERVICE=--output-local-service-test $(LIBRARY_ROOT)/Model
167+
polymorph_net: OUTPUT_LOCAL_SERVICE=--local-service-test
168168
polymorph_net: _polymorph_wrapped
169169
polymorph_net: POLYMORPH_LANGUAGE_TARGET=net
170170
polymorph_net: _polymorph_dependencies

codegen/smithy-dafny-codegen-cli/README.md

Lines changed: 25 additions & 26 deletions
Original file line numberDiff line numberDiff line change
@@ -26,27 +26,30 @@ BUILD SUCCESSFUL in 507ms
2626

2727
$ # run help
2828
$ ./gradlew run --args="-h"
29+
30+
> Task :run
2931
usage: smithy-dafny-codegen-cli
30-
--aws-sdk <optional> generate AWS SDK-style
31-
API and shims
32-
-d,--dependent-model <arg> directory for dependent model
33-
file[s] (.smithy format)
34-
-h,--help print help message
35-
--include-dafny <arg> <optional> file to be include in
36-
the Dafny model file
37-
-m,--model <arg> directory for the model file[s]
38-
(.smithy format). Also the Dafny
39-
output directory.
40-
-n,--namespace <arg> smithy namespace to generate code
41-
for, such as 'com.foo'
42-
--output-dafny <optional> generate Dafny code
43-
--output-dotnet <arg> <optional> output directory for
44-
generated .NET files
45-
--output-java <arg> <optional> output directory for
46-
generated Java files
47-
--output-local-service-test <arg> <optional> output directory for
48-
generated Dafny that tests a local
49-
service
32+
--aws-sdk <optional> generate AWS SDK-style API
33+
and shims
34+
-d,--dependent-model <arg> directory for dependent model file[s]
35+
(.smithy format)
36+
-h,--help print help message
37+
--include-dafny <arg> <optional> files to be include in the
38+
generated Dafny
39+
--java-aws-sdk-version <arg> <optional> AWS SDK for Java version to
40+
use: v1, or v2 (default)
41+
--local-service-test <optional> generate Dafny that tests a
42+
local service
43+
-m,--model <arg> directory for the model file[s]
44+
(.smithy or json format).
45+
-n,--namespace <arg> smithy namespace to generate code for,
46+
such as 'com.foo'
47+
--output-dafny <arg> <optional> output directory for
48+
generated Dafny code
49+
--output-dotnet <arg> <optional> output directory for
50+
generated .NET files
51+
--output-java <arg> <optional> output directory for
52+
generated Java files
5053

5154

5255
BUILD SUCCESSFUL in 839ms
@@ -57,7 +60,7 @@ $ # generate local service in Dafny, Java, & .NET
5760
$ DAFNY_ROOT=../../../private-aws-encryption-sdk-dafny-staging
5861
$ AwsCryptographyPrimitives_ROOT=$DAFNY_ROOT/AwsCryptographyPrimitives
5962
$./gradlew run --args="\
60-
--output-dafny \
63+
--output-dafny $AwsCryptographyPrimitives_ROOT/Model\
6164
--include-dafny $DAFNY_ROOT/StandardLibrary/src/Index.dfy \
6265
--output-dotnet $AwsCryptographyPrimitives_ROOT/runtimes/net/Generated/ \
6366
--output-java $AwsCryptographyPrimitives_ROOT/runtimes/java/src/main/smithy-generated \
@@ -75,11 +78,7 @@ You can also look at the [ServiceCodegenSmokeTest](./src/test/java/software/amaz
7578
## Arguments
7679
By default, nothing is generated.
7780
Language generation is enabled by the language's `output` argument.
78-
For `dotnet` and `java`, this argument also determines the directory code will be written.
79-
For `dafny`, by default, the code will be written to the `model` directory.
80-
If the `output-local-service-test` option is provided,
81-
the Dafny code will be written there.
82-
81+
This argument also determines the directory code will be written.
8382

8483
## Useful Debugging expressions:
8584

Lines changed: 89 additions & 89 deletions
Original file line numberDiff line numberDiff line change
@@ -1,89 +1,89 @@
1-
@rem
2-
@rem Copyright 2015 the original author or authors.
3-
@rem
4-
@rem Licensed under the Apache License, Version 2.0 (the "License");
5-
@rem you may not use this file except in compliance with the License.
6-
@rem You may obtain a copy of the License at
7-
@rem
8-
@rem https://www.apache.org/licenses/LICENSE-2.0
9-
@rem
10-
@rem Unless required by applicable law or agreed to in writing, software
11-
@rem distributed under the License is distributed on an "AS IS" BASIS,
12-
@rem WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
13-
@rem See the License for the specific language governing permissions and
14-
@rem limitations under the License.
15-
@rem
16-
17-
@if "%DEBUG%" == "" @echo off
18-
@rem ##########################################################################
19-
@rem
20-
@rem Gradle startup script for Windows
21-
@rem
22-
@rem ##########################################################################
23-
24-
@rem Set local scope for the variables with windows NT shell
25-
if "%OS%"=="Windows_NT" setlocal
26-
27-
set DIRNAME=%~dp0
28-
if "%DIRNAME%" == "" set DIRNAME=.
29-
set APP_BASE_NAME=%~n0
30-
set APP_HOME=%DIRNAME%
31-
32-
@rem Resolve any "." and ".." in APP_HOME to make it shorter.
33-
for %%i in ("%APP_HOME%") do set APP_HOME=%%~fi
34-
35-
@rem Add default JVM options here. You can also use JAVA_OPTS and GRADLE_OPTS to pass JVM options to this script.
36-
set DEFAULT_JVM_OPTS="-Xmx64m" "-Xms64m"
37-
38-
@rem Find java.exe
39-
if defined JAVA_HOME goto findJavaFromJavaHome
40-
41-
set JAVA_EXE=java.exe
42-
%JAVA_EXE% -version >NUL 2>&1
43-
if "%ERRORLEVEL%" == "0" goto execute
44-
45-
echo.
46-
echo ERROR: JAVA_HOME is not set and no 'java' command could be found in your PATH.
47-
echo.
48-
echo Please set the JAVA_HOME variable in your environment to match the
49-
echo location of your Java installation.
50-
51-
goto fail
52-
53-
:findJavaFromJavaHome
54-
set JAVA_HOME=%JAVA_HOME:"=%
55-
set JAVA_EXE=%JAVA_HOME%/bin/java.exe
56-
57-
if exist "%JAVA_EXE%" goto execute
58-
59-
echo.
60-
echo ERROR: JAVA_HOME is set to an invalid directory: %JAVA_HOME%
61-
echo.
62-
echo Please set the JAVA_HOME variable in your environment to match the
63-
echo location of your Java installation.
64-
65-
goto fail
66-
67-
:execute
68-
@rem Setup the command line
69-
70-
set CLASSPATH=%APP_HOME%\gradle\wrapper\gradle-wrapper.jar
71-
72-
73-
@rem Execute Gradle
74-
"%JAVA_EXE%" %DEFAULT_JVM_OPTS% %JAVA_OPTS% %GRADLE_OPTS% "-Dorg.gradle.appname=%APP_BASE_NAME%" -classpath "%CLASSPATH%" org.gradle.wrapper.GradleWrapperMain %*
75-
76-
:end
77-
@rem End local scope for the variables with windows NT shell
78-
if "%ERRORLEVEL%"=="0" goto mainEnd
79-
80-
:fail
81-
rem Set variable GRADLE_EXIT_CONSOLE if you need the _script_ return code instead of
82-
rem the _cmd.exe /c_ return code!
83-
if not "" == "%GRADLE_EXIT_CONSOLE%" exit 1
84-
exit /b 1
85-
86-
:mainEnd
87-
if "%OS%"=="Windows_NT" endlocal
88-
89-
:omega
1+
@rem
2+
@rem Copyright 2015 the original author or authors.
3+
@rem
4+
@rem Licensed under the Apache License, Version 2.0 (the "License");
5+
@rem you may not use this file except in compliance with the License.
6+
@rem You may obtain a copy of the License at
7+
@rem
8+
@rem https://www.apache.org/licenses/LICENSE-2.0
9+
@rem
10+
@rem Unless required by applicable law or agreed to in writing, software
11+
@rem distributed under the License is distributed on an "AS IS" BASIS,
12+
@rem WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
13+
@rem See the License for the specific language governing permissions and
14+
@rem limitations under the License.
15+
@rem
16+
17+
@if "%DEBUG%" == "" @echo off
18+
@rem ##########################################################################
19+
@rem
20+
@rem Gradle startup script for Windows
21+
@rem
22+
@rem ##########################################################################
23+
24+
@rem Set local scope for the variables with windows NT shell
25+
if "%OS%"=="Windows_NT" setlocal
26+
27+
set DIRNAME=%~dp0
28+
if "%DIRNAME%" == "" set DIRNAME=.
29+
set APP_BASE_NAME=%~n0
30+
set APP_HOME=%DIRNAME%
31+
32+
@rem Resolve any "." and ".." in APP_HOME to make it shorter.
33+
for %%i in ("%APP_HOME%") do set APP_HOME=%%~fi
34+
35+
@rem Add default JVM options here. You can also use JAVA_OPTS and GRADLE_OPTS to pass JVM options to this script.
36+
set DEFAULT_JVM_OPTS="-Xmx64m" "-Xms64m"
37+
38+
@rem Find java.exe
39+
if defined JAVA_HOME goto findJavaFromJavaHome
40+
41+
set JAVA_EXE=java.exe
42+
%JAVA_EXE% -version >NUL 2>&1
43+
if "%ERRORLEVEL%" == "0" goto execute
44+
45+
echo.
46+
echo ERROR: JAVA_HOME is not set and no 'java' command could be found in your PATH.
47+
echo.
48+
echo Please set the JAVA_HOME variable in your environment to match the
49+
echo location of your Java installation.
50+
51+
goto fail
52+
53+
:findJavaFromJavaHome
54+
set JAVA_HOME=%JAVA_HOME:"=%
55+
set JAVA_EXE=%JAVA_HOME%/bin/java.exe
56+
57+
if exist "%JAVA_EXE%" goto execute
58+
59+
echo.
60+
echo ERROR: JAVA_HOME is set to an invalid directory: %JAVA_HOME%
61+
echo.
62+
echo Please set the JAVA_HOME variable in your environment to match the
63+
echo location of your Java installation.
64+
65+
goto fail
66+
67+
:execute
68+
@rem Setup the command line
69+
70+
set CLASSPATH=%APP_HOME%\gradle\wrapper\gradle-wrapper.jar
71+
72+
73+
@rem Execute Gradle
74+
"%JAVA_EXE%" %DEFAULT_JVM_OPTS% %JAVA_OPTS% %GRADLE_OPTS% "-Dorg.gradle.appname=%APP_BASE_NAME%" -classpath "%CLASSPATH%" org.gradle.wrapper.GradleWrapperMain %*
75+
76+
:end
77+
@rem End local scope for the variables with windows NT shell
78+
if "%ERRORLEVEL%"=="0" goto mainEnd
79+
80+
:fail
81+
rem Set variable GRADLE_EXIT_CONSOLE if you need the _script_ return code instead of
82+
rem the _cmd.exe /c_ return code!
83+
if not "" == "%GRADLE_EXIT_CONSOLE%" exit 1
84+
exit /b 1
85+
86+
:mainEnd
87+
if "%OS%"=="Windows_NT" endlocal
88+
89+
:omega

0 commit comments

Comments
 (0)