Update doo files without rebuilding to avoid Z3 timeout issues (#6337)

## Problem
During minor version patches, the current version bump process rebuilds
standard libraries with the new version. However, when the build machine
has a different version of Z3, the standard libraries sometimes timeout,
making the build process non-deterministic.

## Solution
This PR modifies the version bump script to update doo files without
rebuilding them:

1. **For standard library doo files**: Instead of running `make -C
Source/DafnyStandardLibraries update-binary`, the script now:
   - Unzips each doo file (which are actually zip archives)
   - Updates the `dafny_version` field in the `manifest.toml` file
   - Rezips the file

2. **For test doo files**: Instead of rebuilding from source, the script
updates the version in the existing doo files using the same approach.

## Files Modified
- `Scripts/bump_version_number.js`: Added `updateDooVersion` function
and replaced rebuild logic
- `docs/dev/VERSIONBUMP.md`: Updated documentation to reflect the new
approach

## Testing
- Tested in test mode with version 4.10.2
- Verified that doo files are correctly updated with new version numbers
- All existing functionality for updating other version references
remains intact

## ⚠️ Important Note
**This PR was created using Amazon Q and requires careful review.**

## Benefits
- Makes version bumps more deterministic
- Avoids Z3 timeout issues on machines with different Z3 versions
- Faster version bump process (no compilation required)
- Maintains the same end result (updated version numbers in doo files)

Author: MikaelMayer

Scripts/bump_version_number.js

@@ -43,26 +43,35 @@ async function synchronizeRepositoryWithNewVersionNumber() {
   } else {
     await bumpVersionNumber(version);
   }
-  //# * Compile Dafny to ensure you have the right version number.
-  await execute("make exe");
-
-  //# * Compile the standard libraries and update their binaries which are checked in
-  await executeWithTimeout("make -C Source/DafnyStandardLibraries update-binary", 50*minutes);
+  //# * Update standard library doo files instead of rebuilding to avoid Z3 timeout issues
+  const standardLibraryDir = "Source/DafnyStandardLibraries/binaries";
+  const standardLibraryDooFiles = fs.readdirSync(standardLibraryDir)
+    .filter(file => file.endsWith('.doo'))
+    .map(file => `${standardLibraryDir}/${file}`);
+
+  for (const dooFile of standardLibraryDooFiles) {
+    await updateDooVersion(dooFile, version);
+  }
 
   // Verify that binaries have been updated.
   await sanityCheckStandardLibraries(version);
 
-  //# * Recompile Dafny so that standard libraries are in the executable.
-  await execute("make exe");
-  
   //# * In the test directory `Source/IntegrationTests/TestFiles/LitTests/LitTest`,
-  await execute(
-  //#   * Rebuild `pythonmodule/multimodule/PythonModule1.doo` from `pythonmodule/multimodule/dafnysource/helloworld.dfy`
-  `bash Scripts/dafny build -t:lib ${TestDirectory}/pythonmodule/multimodule/dafnysource/helloworld.dfy -o ${TestDirectory}/pythonmodule/multimodule/PythonModule1.doo`,
-  //#   * Rebuild `pythonmodule/nestedmodule/SomeNestedModule.doo` from `pythonmodule/nestedmodule/dafnysource/SomeNestedModule.dfy`
-  `bash Scripts/dafny build -t:lib ${TestDirectory}/pythonmodule/nestedmodule/dafnysource/SomeNestedModule.dfy -o ${TestDirectory}/pythonmodule/nestedmodule/SomeNestedModule.doo`,
-  //#   * Rebuild `gomodule/multimodule/test.doo` from `gomodule/multimodule/dafnysource/helloworld.dfy`
-  `bash Scripts/dafny build -t:lib ${TestDirectory}/gomodule/multimodule/dafnysource/helloworld.dfy -o ${TestDirectory}/gomodule/multimodule/test.doo`);
+  //# * Update test doo files instead of rebuilding
+  //#   * Update `pythonmodule/multimodule/PythonModule1.doo` version
+  //#   * Update `pythonmodule/nestedmodule/SomeNestedModule.doo` version
+  //#   * Update `gomodule/multimodule/test.doo` version
+  const testDooFiles = [
+    `${TestDirectory}/pythonmodule/multimodule/PythonModule1.doo`,
+    `${TestDirectory}/pythonmodule/nestedmodule/SomeNestedModule.doo`,
+    `${TestDirectory}/gomodule/multimodule/test.doo`
+  ];
+
+  for (const dooFile of testDooFiles) {
+    if (fs.existsSync(dooFile)) {
+      await updateDooVersion(dooFile, version);
+    }
+  }
 
   //#   * Search for `dafny_version = ` in checked-in `.dtr` files of the `<TestDirectory>`
   //#    and update the version number.
@@ -100,6 +109,41 @@ async function synchronizeRepositoryWithNewVersionNumber() {
     `Source/DafnyRuntime/DafnyRuntime.csproj`, existingVersion);
 }
 
+async function updateDooVersion(dooPath, newVersion) {
+  const tempDir = `${dooPath}_temp`;
+  
+  try {
+    // Create temp directory
+    await execAsync(`mkdir -p "${tempDir}"`);
+    
+    // Unzip doo file
+    await execAsync(`unzip -o "${dooPath}" -d "${tempDir}"`);
+    
+    // Read manifest.toml
+    const manifestPath = `${tempDir}/manifest.toml`;
+    let manifestContent = await fs.promises.readFile(manifestPath, 'utf-8');
+    
+    // Update version
+    manifestContent = manifestContent.replace(
+      /dafny_version = "(\d+\.\d+\.\d+)\.0"/,
+      `dafny_version = "${newVersion}.0"`
+    );
+    
+    // Write updated manifest
+    await fs.promises.writeFile(manifestPath, manifestContent);
+    
+    // Rezip
+    const fileName = dooPath.split('/').pop();
+    await execAsync(`cd "${tempDir}" && zip -r "../${fileName}_new" *`);
+    await execAsync(`mv "${tempDir}/../${fileName}_new" "${dooPath}"`);
+    
+    console.log(`Updated ${dooPath} to version ${newVersion}`);
+  } finally {
+    // Cleanup
+    await execAsync(`rm -rf "${tempDir}"`).catch(() => {});
+  }
+}
+
 // Unzips the file Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries.doo (it's actually a zip file)
 // Fetch the content of Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries/manifest.toml
 // Verify that dafny_version = "Major.Minor.Patch.0" corresponds ot the version that is provided

docs/dev/VERSIONBUMP.md

@@ -23,13 +23,12 @@ verifies that this file is in sync with that script.
 
 Assuming `<TestDirectory>` to be `Source/IntegrationTests/TestFiles/LitTests/LitTest`,
 perform the following:
-* Compile Dafny to ensure you have the right version number.
-* Compile the standard libraries and update their binaries which are checked in
-* Recompile Dafny so that standard libraries are in the executable.
+* Update standard library doo files instead of rebuilding to avoid Z3 timeout issues
 * In the test directory `Source/IntegrationTests/TestFiles/LitTests/LitTest`,
-  * Rebuild `pythonmodule/multimodule/PythonModule1.doo` from `pythonmodule/multimodule/dafnysource/helloworld.dfy`
-  * Rebuild `pythonmodule/nestedmodule/SomeNestedModule.doo` from `pythonmodule/nestedmodule/dafnysource/SomeNestedModule.dfy`
-  * Rebuild `gomodule/multimodule/test.doo` from `gomodule/multimodule/dafnysource/helloworld.dfy`
+* Update test doo files instead of rebuilding
+  * Update `pythonmodule/multimodule/PythonModule1.doo` version
+  * Update `pythonmodule/nestedmodule/SomeNestedModule.doo` version
+  * Update `gomodule/multimodule/test.doo` version
   * Search for `dafny_version = ` in checked-in `.dtr` files of the `<TestDirectory>`
    and update the version number.
     Except for the file NoGood.dtr which is not valid.