refactoring: simplify the passing of tla modules, matching the interface of tlatools

FedericoPonzi · FedericoPonzi · commit 8650b1758875 · 2026-02-11T22:46:27.000Z
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
@@ -40,10 +40,7 @@ jobs:
         uses: gradle/actions/setup-gradle@v5
 
       - name: Build with Gradle Wrapper
-        env:
-          TLAPS_LIBRARY: ${{ github.workspace }}/tlapm/library
-          TLA_COMMUNITY_MODULES: ${{ github.workspace }}/CommunityModules
-        run: ./gradlew build
+        run: ./gradlew build -DTLA-Library="${{ github.workspace }}/tlapm/library:${{ github.workspace }}/CommunityModules"
 
       - name: Upload SpotBugs report
         if: always()
diff --git a/.github/workflows/semantic-preservation.yml b/.github/workflows/semantic-preservation.yml
@@ -51,11 +51,7 @@ jobs:
         uses: gradle/actions/setup-gradle@v5
 
       - name: Run semantic preservation tests
-        env:
-          TLA_COMMUNITY_MODULES: ${{ github.workspace }}/CommunityModules
-          TLAPS_LIBRARY: ${{ github.workspace }}/tlapm/library
-          APALACHE_HOME: ${{ github.workspace }}/apalache
-        run: ./gradlew semanticPreservationTest -Dtlaplus.examples.path=${{ github.workspace }}/tlaplus-examples
+        run: ./gradlew semanticPreservationTest -Dtlaplus.examples.path=${{ github.workspace }}/tlaplus-examples -DTLA-Library="${{ github.workspace }}/tlapm/library:${{ github.workspace }}/CommunityModules:${{ github.workspace }}/apalache/src/tla"
 
       - name: Upload test results
         uses: actions/upload-artifact@v6
diff --git a/README.md b/README.md
@@ -58,9 +58,25 @@ It will print your reformatted spec in output. If the optional "OUTFILE" paramet
 output to that file.
 You can use the input file as the output file as well. Run with `-help` parameter for the help text.
 
+### Module search paths
+
+If your spec uses `EXTENDS` to reference modules that are not in the same directory (e.g., TLAPS, Community Modules,
+or custom libraries), you can pass their locations via the `-DTLA-Library` JVM system property:
+
+```
+java -DTLA-Library=/path/to/tlaps/library:/path/to/CommunityModules -jar tlaplus-formatter.jar MySpec.tla
+```
+
+Multiple paths are separated by `:` on Linux/macOS or `;` on Windows. Standard modules (Naturals, Sequences,
+FiniteSets, TLC, etc.) are bundled with the formatter and do not need to be specified.
+
 ## VSCode integration
 
-It's a work in progress, see [PR-327](https://github.com/tlaplus/vscode-tlaplus/pull/327/files) on vscode-tlaplus repo.
+The formatter is integrated into the [TLA+ VSCode extension](https://github.com/tlaplus/vscode-tlaplus). Use the
+standard "Format Document" command (`Shift+Alt+F`) to format TLA+ files. The extension automatically passes your
+configured `tlaplus.moduleSearchPaths` to the formatter.
+
+You can disable the formatter via the `tlaplus.formatter.enabled` setting.
 
 ## Limitations
 
diff --git a/build.gradle.kts b/build.gradle.kts
@@ -63,6 +63,7 @@ tasks.withType<Copy> {
 tasks.test {
     useJUnitPlatform()
     finalizedBy(tasks.jacocoTestReport)
+    System.getProperty("TLA-Library")?.let { systemProperty("TLA-Library", it) }
 }
 
 tasks.jacocoTestReport {
@@ -80,6 +81,7 @@ tasks.register<Test>("semanticPreservationTest") {
     }
     systemProperties(System.getProperties().filter { (k, _) -> k.toString().startsWith("tlaplus.") }
         .map { (k, v) -> k.toString() to v.toString() }.toMap())
+    System.getProperty("TLA-Library")?.let { systemProperty("TLA-Library", it) }
 }
 
 tasks.register("generateVersionProperties") {
diff --git a/src/main/java/me/fponzi/tlaplusformatter/SANYWrapper.java b/src/main/java/me/fponzi/tlaplusformatter/SANYWrapper.java
@@ -30,8 +30,9 @@ public static TreeNode load(File file) throws IOException, SanyFrontendException
 
         String parentDirPath = file.getAbsoluteFile().getParent();
 
-        // Resolver for filenames, patched for wired modules.
-        var filenameResolver = new CustomFilenameToStream(parentDirPath);
+        // Build library paths: parent dir + any paths from -DTLA-Library
+        var libraryPaths = buildLibraryPaths(parentDirPath);
+        var filenameResolver = new CustomFilenameToStream(libraryPaths);
 
         // Set a unique tmpdir to avoid race-condition in SANY
         // TODO: RM once https://github.com/tlaplus/tlaplus/issues/688 is fixed
@@ -43,6 +44,27 @@ public static TreeNode load(File file) throws IOException, SanyFrontendException
         return parseUnitContext.get(specObj.getRootModule().getName().toString()).getParseTree();
     }
 
+    /**
+     * Builds the array of library paths for SANY's module resolution.
+     * Includes the parent directory of the spec file and any paths
+     * specified via the -DTLA-Library system property.
+     */
+    static String[] buildLibraryPaths(String parentDirPath) {
+        List<String> paths = new ArrayList<>();
+        paths.add(parentDirPath);
+
+        String tlaLibrary = System.getProperty(SimpleFilenameToStream.TLA_LIBRARY);
+        if (tlaLibrary != null && !tlaLibrary.isEmpty()) {
+            for (String p : tlaLibrary.split(File.pathSeparator)) {
+                if (!p.isEmpty()) {
+                    paths.add(p);
+                }
+            }
+        }
+
+        return paths.toArray(new String[0]);
+    }
+
     public static void loadSpecObject(SpecObj specObj, File file, StringWriter errBuf) throws IOException, SanyFrontendException {
         var outStream = WriterOutputStream
                 .builder()
@@ -88,65 +110,9 @@ private static void ThrowOnError(SpecObj specObj) {
     }
 
     private static class CustomFilenameToStream extends SimpleFilenameToStream {
-        private final List<String> additionalPaths;
-
-        public CustomFilenameToStream(String parentDirPath) {
-            super(parentDirPath);
-            this.additionalPaths = getAdditionalModulePaths();
+        public CustomFilenameToStream(String[] libraryPaths) {
+            super(libraryPaths);
             this.tmpDir.toFile().deleteOnExit();
         }
-
-        private static List<String> getAdditionalModulePaths() {
-            List<String> paths = new ArrayList<>();
-            // Check for community modules, TLAPS, and Apalache in common locations
-            String[] possiblePaths = {
-                    // Community modules
-                    System.getenv("TLA_COMMUNITY_MODULES"),
-                    "/tmp/CommunityModules/modules",
-                    "/tmp/CommunityModules",
-                    System.getProperty("user.home") + "/.tlaplus/CommunityModules/modules",
-                    // TLAPS library
-                    System.getenv("TLAPS_LIBRARY"),
-                    "/tmp/tlapm/library",
-                    System.getProperty("user.home") + "/.tlaplus/tlaps/library",
-                    "/usr/local/lib/tlaps/library",
-                    // Apalache modules
-                    System.getenv("APALACHE_HOME") != null ? System.getenv("APALACHE_HOME") + "/src/tla" : null,
-                    "/tmp/apalache/src/tla",
-                    System.getProperty("user.home") + "/.tlaplus/apalache/src/tla"
-            };
-            for (String path : possiblePaths) {
-                if (path != null) {
-                    File dir = new File(path);
-                    if (dir.exists() && dir.isDirectory()) {
-                        paths.add(path);
-                    }
-                }
-            }
-            return paths;
-        }
-
-        @Override
-        public TLAFile resolve(String name, boolean isModule) {
-            // First try with the default resolver.
-            TLAFile sourceFile = super.resolve(name, isModule);
-            if (sourceFile != null && sourceFile.exists()) {
-                return sourceFile;
-            }
-
-            // Try additional paths (community modules, etc.)
-            // name already includes .tla extension when isModule=true
-            String filename = name.endsWith(".tla") ? name : name + ".tla";
-            for (String path : additionalPaths) {
-                File file = new File(path, filename);
-                if (file.exists()) {
-                    return new TLAFile(file.getAbsolutePath(), this);
-                }
-            }
-
-            // Return the result from parent resolver (non-existent TLAFile, not null)
-            // to preserve SANY's expected behavior
-            return sourceFile;
-        }
     }
 }

Original file line number	Diff line number	Diff line change
`@@ -63,6 +63,7 @@ tasks.withType<Copy> {`
`63`	`63`	`tasks.test {`
`64`	`64`	`useJUnitPlatform()`
`65`	`65`	`finalizedBy(tasks.jacocoTestReport)`
	`66`	`+ System.getProperty("TLA-Library")?.let { systemProperty("TLA-Library", it) }`
`66`	`67`	`}`
`67`	`68`
`68`	`69`	`tasks.jacocoTestReport {`
`@@ -80,6 +81,7 @@ tasks.register<Test>("semanticPreservationTest") {`
`80`	`81`	`}`
`81`	`82`	`systemProperties(System.getProperties().filter { (k, _) -> k.toString().startsWith("tlaplus.") }`
`82`	`83`	`.map { (k, v) -> k.toString() to v.toString() }.toMap())`
	`84`	`+ System.getProperty("TLA-Library")?.let { systemProperty("TLA-Library", it) }`
`83`	`85`	`}`
`84`	`86`
`85`	`87`	`tasks.register("generateVersionProperties") {`