clean oleans + precomp sed

Author: xgenereux

Benchmark/RunTrans.lean

@@ -12,5 +12,5 @@ import Benchmark.Trans
 
 -- TODO : replace with 6!!
 -- /- Transitivity benchmark -/
-bchmk 1 with pows 5  using trans 0
-bchmk 1 with pows 5  using trans 100
+bchmk 1 with pows 4  using trans 0
+bchmk 1 with pows 4  using trans 100

run-benchmark.sh

@@ -4,6 +4,45 @@
 # CONFIGURATION
 # ==============================================================================
 
+# Default value for precompileModules
+PRECOMP=false
+
+# Time format
+TIMEFORMAT="this took %R seconds"
+
+# Parse command line arguments
+while [[ $# -gt 0 ]]; do
+    case $1 in
+        --precomp)
+            PRECOMP="$2"
+            shift 2
+            ;;
+        *)
+            echo "Unknown option: $1"
+            echo "Usage: $0 [--precomp true|false]"
+            exit 1
+            ;;
+    esac
+done
+
+# Validate precomp value
+if [[ "$PRECOMP" != "true" && "$PRECOMP" != "false" ]]; then
+    echo "Error: --precomp must be 'true' or 'false'"
+    exit 1
+fi
+
+# Modify lakefile.toml
+echo "--- Setting precompileModules = $PRECOMP in lakefile.toml ---"
+if [[ -f "lakefile.toml" ]]; then
+    # Use sed to replace the precompileModules line
+    # This handles various formats: precompileModules = true/false with/without quotes
+    # Empty string after -i means no backup (works on both Linux and macOS)
+    sed -i '' "s/^precompileModules = .*/precompileModules = $PRECOMP/" lakefile.toml
+    echo "Updated lakefile.toml"
+else
+    echo "Warning: lakefile.toml not found"
+fi
+
 cmd_trans() {
     lake build Benchmark.RunTrans
 }
@@ -41,15 +80,16 @@ parse_lean_output() {
     '
 }
 
-TIMEFORMAT="this took %R seconds"
+echo "--- Deleting .oleans ---"
+lake clean
 
 echo "--- Running Benchmark: Transitivity ---"
 # Capture output and evaluate it
 eval $(time cmd_trans | parse_lean_output "FIG1_")
 
 
 echo "--- Running Benchmark: Depth ---"
-time eval $(cmd_depth | parse_lean_output "FIG2_")
+eval $(time cmd_depth | parse_lean_output "FIG2_")
 
 {
     echo "Transitivity Benchmark"
@@ -175,4 +215,4 @@ if command -v pdflatex &> /dev/null; then
     echo "Done! Generated benchmark_results.pdf"
 else
     echo "Warning: pdflatex not found. The .tex file was created but not compiled."
-fi
+fi