fix: Support Windows properly (#662)

*Issue #, if available:* Resolves #317 (AFAICT - the logs from the linked run have expired. But the CI now exercises codegen on Windows, which gives me confidence it should work. We can open new issues if we discover new issues) *Description of changes:* Addresses a handful of portability issues, so that Windows is supported: 1. Remove `check_dafny_version.sh` and extract/check the Dafny version in Java code instead (and updated `DafnyVersion` to handle the `+build` part of the semver 2.0). `--dafny-version` is now an optional parameter, provided just in case you want to override it. 2. Avoid the false error about the `project.properties` path containing a `:` (which it usually does on Windows), despite it not being a templated path. Also renamed an overload to the more specific `evalTemplateResource` to make the distinction clearer. 3. Replace `shell pwd` in the makefile with the more portable `$(CURDIR)`. Added building a target on the SimpleString test model on Windows as a sanity check. I attempted building all models on all platforms, but besides this being expensive, my last attempt saw windows jobs hang for some reason. Would like to revisit that but later, as this PR definitely moves us forward. Big thanks to @MikaelMayer for helping to figure out some of these fixes. :)
smithy-lang · Oct 24, 2024 · 7a0878e · 7a0878e
1 parent e602cbf
commit 7a0878e
Show file tree

Hide file tree

Showing 12 changed files with 191 additions and 160 deletions.
diff --git a/.github/workflows/smithy-polymorph.yml b/.github/workflows/smithy-polymorph.yml
@@ -21,15 +21,10 @@ jobs:
         with:
           distribution: "corretto"
           java-version: "17"
-      - uses: actions/setup-java@v3
-        with:
-          distribution: "corretto"
-          java-version: "17"
       - name: Setup Dafny
         uses: dafny-lang/[email protected]
         with:
-          # Matching the hard-coded version for the "2023" edition for now
-          dafny-version: 4.1.0
+          dafny-version: 4.8.1
 
       - name: Install Smithy-Dafny codegen dependencies
         uses: ./.github/actions/install_smithy_dafny_codegen_dependencies
@@ -46,6 +41,11 @@ jobs:
           arguments: :smithy-dafny-codegen:test
           build-root-directory: codegen
 
+      - name: Build a test model (just to test multiple OS')
+        shell: bash
+        working-directory: TestModels/SimpleTypes/SimpleString
+        run: make polymorph_dafny
+
       - name: not-grep
         if: matrix.os == 'ubuntu-latest'
         uses: mattsb42-meta/[email protected]
diff --git a/SmithyDafnyMakefile.mk b/SmithyDafnyMakefile.mk
@@ -39,7 +39,7 @@ VERIFY_TIMEOUT := 100
 
 # This evaluates to the path of the current working directory.
 # i.e. The specific library under consideration.
-LIBRARY_ROOT := $(shell pwd)
+LIBRARY_ROOT := $(CURDIR)
 # Smithy Dafny code gen needs to know
 # where the smithy model is.
 # This is generally in the same directory as the library.
@@ -56,8 +56,6 @@ SMITHY_MODEL_ROOT := $(LIBRARY_ROOT)/Model
 CODEGEN_CLI_ROOT := $(SMITHY_DAFNY_ROOT)/codegen/smithy-dafny-codegen-cli
 GRADLEW := $(SMITHY_DAFNY_ROOT)/codegen/gradlew
 
-DAFNY_VERSION := $(shell $(SMITHY_DAFNY_ROOT)/scripts/check_dafny_version.sh)
-
 include $(SMITHY_DAFNY_ROOT)/SmithyDafnySedMakefile.mk
 
 # This flag enables pre-processing on extern module names.
@@ -276,7 +274,6 @@ _polymorph: mvn_local_deploy_polymorph_dependencies
 _polymorph:
 	cd $(CODEGEN_CLI_ROOT); \
 	./../gradlew run --args="\
-	--dafny-version $(DAFNY_VERSION) \
 	--library-root $(LIBRARY_ROOT) \
 	--patch-files-dir $(if $(DIR_STRUCTURE_V2),$(LIBRARY_ROOT)/codegen-patches/$(SERVICE),$(LIBRARY_ROOT)/codegen-patches) \
 	--properties-file $(LIBRARY_ROOT)/project.properties \
@@ -303,7 +300,6 @@ _polymorph_wrapped:
 	@: $(if ${CODEGEN_CLI_ROOT},,$(error You must pass the path CODEGEN_CLI_ROOT: CODEGEN_CLI_ROOT=/path/to/smithy-dafny/codegen/smithy-dafny-codegen-cli));
 	cd $(CODEGEN_CLI_ROOT); \
 	./../gradlew run --args="\
-	--dafny-version $(DAFNY_VERSION) \
 	--library-root $(LIBRARY_ROOT) \
 	--properties-file $(LIBRARY_ROOT)/project.properties \
 	$(INPUT_DAFNY) \
@@ -604,7 +600,6 @@ _patch_after_transpile_rust:
 	cd $(CODEGEN_CLI_ROOT); \
 	./../gradlew run --args="\
 	patch-after-transpile \
-	--dafny-version $(DAFNY_VERSION) \
 	--library-root $(LIBRARY_ROOT) \
 	$(OUTPUT_RUST) \
 	--model $(if $(DIR_STRUCTURE_V2), $(LIBRARY_ROOT)/dafny/$(SERVICE)/Model, $(SMITHY_MODEL_ROOT)) \

diff --git a/TestModels/dafny-dependencies/StandardLibrary/Makefile b/TestModels/dafny-dependencies/StandardLibrary/Makefile
@@ -26,7 +26,6 @@ endif
 polymorph_dafny :
 	cd $(CODEGEN_CLI_ROOT); \
 	$(GRADLEW) run --args="\
-	--dafny-version $(DAFNY_VERSION) \
 	--library-root $(LIBRARY_ROOT) \
 	--properties-file $(PROJECT_ROOT)/$(STD_LIBRARY)/project.properties \
 	--model $(PROJECT_ROOT)/$(STD_LIBRARY)/Model \

diff --git a/codegen/smithy-dafny-codegen-cli/src/main/java/software/amazon/polymorph/CodegenCli.java b/codegen/smithy-dafny-codegen-cli/src/main/java/software/amazon/polymorph/CodegenCli.java
@@ -588,17 +588,15 @@ static Optional<CliArguments> parse(String[] args) throws ParseException {
         }
       }
 
-      DafnyVersion dafnyVersion;
+      DafnyVersion dafnyVersion = null;
       String versionStr = commandLine.getOptionValue("dafny-version");
-      if (versionStr == null) {
-        LOGGER.error("--dafny-version option is required");
-        System.exit(-1);
-      }
-      try {
-        dafnyVersion = DafnyVersion.parse(versionStr.trim());
-      } catch (IllegalArgumentException ex) {
-        LOGGER.error("Could not parse --dafny-version: {}", versionStr);
-        throw ex;
+      if (versionStr != null) {
+        try {
+          dafnyVersion = DafnyVersion.parse(versionStr.trim());
+        } catch (IllegalArgumentException ex) {
+          LOGGER.error("Could not parse --dafny-version: {}", versionStr);
+          throw ex;
+        }
       }
 
       Optional<Path> propertiesFile = Optional

diff --git a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/CodegenEngine.java b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/CodegenEngine.java
@@ -5,9 +5,7 @@
 
 import static software.amazon.smithy.utils.CaseUtils.toSnakeCase;
 
-import com.google.common.base.Strings;
 import com.google.common.collect.ImmutableMap;
-import com.google.common.collect.MoreCollectors;
 import com.google.common.collect.Streams;
 import com.squareup.javapoet.ClassName;
 import java.io.IOException;
@@ -52,9 +50,7 @@
 import software.amazon.polymorph.smithypython.awssdk.extensions.DafnyPythonAwsSdkClientCodegenPlugin;
 import software.amazon.polymorph.smithypython.localservice.extensions.DafnyPythonLocalServiceClientCodegenPlugin;
 import software.amazon.polymorph.smithypython.wrappedlocalservice.extensions.DafnyPythonWrappedLocalServiceClientCodegenPlugin;
-import software.amazon.polymorph.smithyrust.generator.AbstractRustShimGenerator;
 import software.amazon.polymorph.smithyrust.generator.MergedServicesGenerator;
-import software.amazon.polymorph.smithyrust.generator.RustAwsSdkShimGenerator;
 import software.amazon.polymorph.smithyrust.generator.RustLibraryShimGenerator;
 import software.amazon.polymorph.traits.LocalServiceTrait;
 import software.amazon.polymorph.utils.DafnyNameResolverHelpers;
@@ -76,6 +72,10 @@ public class CodegenEngine {
     CodegenEngine.class
   );
 
+  private static final DafnyVersion MIN_DAFNY_VERSION = DafnyVersion.parse(
+    "4.5"
+  );
+
   // Used to distinguish different conventions between the CLI
   // and the Smithy build plugin, such as where .NET project files live.
   private final boolean fromSmithyBuildPlugin;
@@ -220,7 +220,13 @@ private void generateProjectPropertiesFile(final Path outputPath)
       "dafnyVersion",
       dafnyVersionString
     );
-    writeTemplatedFile("project.properties", outputPath.toString(), parameters);
+    // Don't use writeTemplatedFile since outputPath is an absolute path
+    final String propertiesFileContent = IOUtils.evalTemplateResource(
+      getClass(),
+      "project.properties",
+      parameters
+    );
+    IOUtils.writeToFile(propertiesFileContent, outputPath.toFile());
   }
 
   private void generateDafny(final Path outputDir) {
@@ -932,7 +938,7 @@ private record CommandResult(int exitCode, String output) {}
   /**
    * Runs the given command and throws an exception if the exit code is nonzero.
    */
-  private String runCommandOrThrow(Path workingDir, String... args) {
+  private static String runCommandOrThrow(Path workingDir, String... args) {
     final CommandResult result = runCommand(workingDir, args);
     if (result.exitCode != 0) {
       throw new RuntimeException(
@@ -945,7 +951,7 @@ private String runCommandOrThrow(Path workingDir, String... args) {
   /**
    * Runs the given command.
    */
-  private CommandResult runCommand(Path workingDir, String... args) {
+  private static CommandResult runCommand(Path workingDir, String... args) {
     final List<String> argsList = List.of(args);
     final StringBuilder output = new StringBuilder();
     final int exitCode = IoUtils.runCommand(
@@ -1003,7 +1009,7 @@ public static class Builder {
       Collections.emptyMap();
     private Map<TargetLanguage, Path> targetLangTestOutputDirs =
       Collections.emptyMap();
-    private DafnyVersion dafnyVersion = new DafnyVersion(4, 1, 0);
+    private DafnyVersion dafnyVersion;
     private Path propertiesFile;
     private AwsSdkVersion javaAwsSdkVersion = AwsSdkVersion.V2;
     private Path includeDafnyFile;
@@ -1235,9 +1241,18 @@ public CodegenEngine build() {
       final Map<TargetLanguage, Path> targetLangTestOutputDirs =
         ImmutableMap.copyOf(targetLangTestOutputDirsRaw);
 
-      final DafnyVersion dafnyVersion = Objects.requireNonNull(
-        this.dafnyVersion
-      );
+      final DafnyVersion dafnyVersion = Optional
+        .ofNullable(this.dafnyVersion)
+        .orElseGet(CodegenEngine::getDafnyVersionFromDafny);
+      if (dafnyVersion.compareTo(MIN_DAFNY_VERSION) < 0) {
+        throw new IllegalStateException(
+          "A minimum Dafny version of " +
+          MIN_DAFNY_VERSION.unparse() +
+          " is required, but found " +
+          dafnyVersion.unparse()
+        );
+      }
+
       final Optional<Path> propertiesFile = Optional
         .ofNullable(this.propertiesFile)
         .map(path -> path.toAbsolutePath().normalize());
@@ -1301,6 +1316,15 @@ public CodegenEngine build() {
     }
   }
 
+  private static DafnyVersion getDafnyVersionFromDafny() {
+    String versionString = runCommandOrThrow(
+      Path.of("."),
+      "dafny",
+      "--version"
+    );
+    return DafnyVersion.parse(versionString.trim());
+  }
+
   public enum TargetLanguage {
     DAFNY,
     JAVA,

diff --git a/...mithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithydafny/DafnyVersion.java b/...mithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithydafny/DafnyVersion.java
@@ -20,41 +20,59 @@ public class DafnyVersion implements Comparable<DafnyVersion> {
   private final int minor;
   private final int patch;
   // Will be non-null only if there was a pre-release suffix
-  private final String suffix;
+  private final String prerelease;
+  // Will be non-null only if there was a build suffix
+  private final String build;
 
   // Anything with a pre-release suffix should be considered less
   // than a matching version without one.
   private static final Comparator<String> SUFFIX_COMPARATOR =
     Comparator.nullsLast(Comparator.naturalOrder());
 
   public static DafnyVersion parse(String versionString) {
-    if (!versionString.matches("[0-9\\.A-Za-z\\-]*")) {
+    if (!versionString.matches("[0-9.A-Za-z\\-+]*")) {
       throw new IllegalArgumentException();
     }
-    int firstHyphenIndex = versionString.indexOf("-");
     String majorMinorPatch = versionString;
     String suffix = null;
+    String build = null;
+
+    int plusIndex = majorMinorPatch.indexOf("+");
+    if (plusIndex >= 0) {
+      build = majorMinorPatch.substring(plusIndex + 1);
+      majorMinorPatch = versionString.substring(0, plusIndex);
+    }
+
+    int firstHyphenIndex = majorMinorPatch.indexOf("-");
     if (firstHyphenIndex >= 0) {
-      majorMinorPatch = versionString.substring(0, firstHyphenIndex);
-      suffix = versionString.substring(firstHyphenIndex + 1);
+      suffix = majorMinorPatch.substring(firstHyphenIndex + 1);
+      majorMinorPatch = majorMinorPatch.substring(0, firstHyphenIndex);
     }
     String[] splitByDots = majorMinorPatch.split("\\.");
     switch (splitByDots.length) {
       case 1:
-        return new DafnyVersion(Integer.parseInt(splitByDots[0]), 0, 0, suffix);
+        return new DafnyVersion(
+          Integer.parseInt(splitByDots[0]),
+          0,
+          0,
+          suffix,
+          build
+        );
       case 2:
         return new DafnyVersion(
           Integer.parseInt(splitByDots[0]),
           Integer.parseInt(splitByDots[1]),
           0,
-          suffix
+          suffix,
+          build
         );
       case 3:
         return new DafnyVersion(
           Integer.parseInt(splitByDots[0]),
           Integer.parseInt(splitByDots[1]),
           Integer.parseInt(splitByDots[2]),
-          suffix
+          suffix,
+          build
         );
       default:
         throw new IllegalArgumentException();
@@ -65,11 +83,22 @@ public DafnyVersion(int major, int minor, int patch) {
     this(major, minor, patch, null);
   }
 
-  public DafnyVersion(int major, int minor, int patch, String suffix) {
+  public DafnyVersion(int major, int minor, int patch, String prerelease) {
+    this(major, minor, patch, prerelease, null);
+  }
+
+  public DafnyVersion(
+    int major,
+    int minor,
+    int patch,
+    String prerelease,
+    String build
+  ) {
     this.major = requireNonNegative(major);
     this.minor = requireNonNegative(minor);
     this.patch = requireNonNegative(patch);
-    this.suffix = suffix;
+    this.prerelease = prerelease;
+    this.build = build;
   }
 
   private int requireNonNegative(int value) {
@@ -91,8 +120,12 @@ public int getPatch() {
     return patch;
   }
 
-  public String getSuffix() {
-    return suffix;
+  public String getPrerelease() {
+    return prerelease;
+  }
+
+  public String getBuild() {
+    return build;
   }
 
   @Override
@@ -108,13 +141,14 @@ public boolean equals(Object o) {
       major == that.major &&
       minor == that.minor &&
       patch == that.patch &&
-      Objects.equals(suffix, that.suffix)
+      Objects.equals(prerelease, that.prerelease) &&
+      Objects.equals(build, that.build)
     );
   }
 
   @Override
   public int hashCode() {
-    return Objects.hash(major, minor, patch, suffix);
+    return Objects.hash(major, minor, patch, prerelease, build);
   }
 
   @Override
@@ -134,7 +168,7 @@ public int compareTo(DafnyVersion other) {
       return patchComparison;
     }
 
-    return SUFFIX_COMPARATOR.compare(this.suffix, other.suffix);
+    return SUFFIX_COMPARATOR.compare(this.prerelease, other.prerelease);
   }
 
   public String unparse() {
@@ -144,9 +178,13 @@ public String unparse() {
     builder.append(minor);
     builder.append('.');
     builder.append(patch);
-    if (suffix != null) {
+    if (prerelease != null) {
       builder.append('-');
-      builder.append(suffix);
+      builder.append(prerelease);
+    }
+    if (build != null) {
+      builder.append('+');
+      builder.append(build);
     }
     return builder.toString();
   }
@@ -161,8 +199,11 @@ public String toString() {
       minor +
       ", patch=" +
       patch +
-      ", suffix='" +
-      suffix +
+      ", prerelease='" +
+      prerelease +
+      '\'' +
+      ", build='" +
+      build +
       '\'' +
       '}'
     );