Revert "feat: benchmark setup (#183)"

This reverts commit 4414dc5.
leanprover · Sep 26, 2024 · 608cebd · 608cebd
1 parent 4414dc5
commit 608cebd
Show file tree

Hide file tree

Showing 12 changed files with 10 additions and 150 deletions.
diff --git a/.github/workflows/makefile.yml b/.github/workflows/makefile.yml
@@ -42,8 +42,3 @@ jobs:
       if : ${{ runner.os == 'macOS' }}
       run: |
           make cosim NUM_TESTS=100
-
-    - name: Run LNSym Benchmarks (Ubuntu)
-      if : ${{ runner.os != 'macOS' }}
-      run: |
-          make benchmarks
diff --git a/Benchmarks.lean b/Benchmarks.lean
diff --git a/Benchmarks/Command.lean b/Benchmarks/Command.lean
diff --git a/Benchmarks/SHA512.lean b/Benchmarks/SHA512.lean
diff --git a/Benchmarks/SHA512_150.lean b/Benchmarks/SHA512_150.lean
diff --git a/Benchmarks/SHA512_225.lean b/Benchmarks/SHA512_225.lean
diff --git a/Benchmarks/SHA512_400.lean b/Benchmarks/SHA512_400.lean
diff --git a/Makefile b/Makefile
@@ -9,10 +9,8 @@ LAKE = lake
 NUM_TESTS?=3
 VERBOSE?=--verbose
 
-.PHONY: all
+.PHONY: all 
 all: specs correctness proofs tests cosim
-# Note that we don't include benchmarks in `all`,
-# to avoid slowing down CI too much
 
 .PHONY: specs
 	time -p $(LAKE) build Specs
@@ -37,12 +35,8 @@ awslc_elf:
 cosim:
 	time -p lake exe lnsym $(VERBOSE) --num-tests $(NUM_TESTS)
 
-.PHONY: benchmarks
-benchmarks:
-	$(LAKE) build Benchmarks
-
 .PHONY: clean clean_all
-clean:
+clean: 
 	$(LAKE) clean
 
 clean_all: clean

diff --git a/README.md b/README.md
@@ -1,5 +1,5 @@
 # LNSym: Native Code Symbolic Simulator in Lean
-[![Makefile CI](https://github.com/leanprover/LNSym/actions/workflows/makefile.yml/badge.svg)](https://github.com/leanprover/LNSym/actions/workflows/makefile.yml)
+[![Makefile CI](https://github.com/leanprover/LNSym/actions/workflows/makefile.yml/badge.svg)](https://github.com/leanprover/LNSym/actions/workflows/makefile.yml) 
 
 LNSym is a symbolic simulator for Armv8 machine-code programs.
 
@@ -41,8 +41,6 @@ native-code programs of interest.
 
 `awslc_elf`: perform ELF loading tests for AWS-LC.
 
-`benchmarks`: run benchmarks for the symbolic simulator.
-
 ### Makefile variables that can be passed in at the command line
 
 `VERBOSE`: Verbose mode; prints disassembly of the instructions being

diff --git a/Tactics/Sym.lean b/Tactics/Sym.lean
@@ -439,13 +439,15 @@ elab "sym_n" whileTac?:(sym_while)? n:num s:(sym_at)? : tactic => do
 
         let goal ← subst goal hEqId
         trace[Tactic.sym] "performed subsitutition in:\n{goal}"
+        traceHeartbeats
 
         replaceMainGoal [goal]
 
     -- Rudimentary aggregation: we feed all the axiomatic effect hypotheses
     -- added while symbolically evaluating to `simp`
     let msg := m!"aggregating (non-)effects"
     withTraceNode `Tactic.sym (fun _ => pure msg) <| withMainContext' do
+      traceHeartbeats "pre"
       let goal? ← LNSymSimp (← getMainGoal) c.aggregateSimpCtx c.aggregateSimprocs
       replaceMainGoal goal?.toList
 

diff --git a/Tactics/SymContext.lean b/Tactics/SymContext.lean
@@ -242,12 +242,12 @@ def inferStatePrefixAndNumber : SymM Unit := do
       state_prefix := (state.get? 0).getD 's' |>.toString,
       currentStateNumber })
   else
-    SymM.logWarning m!"\
-Expected state to be a single letter followed by a number, but found:
-  {state}
+    SymM.logWarning "\
+      Expected state to be a single letter followed by a number, but found:
+        {state}
 
-Falling back to the default numbering scheme, \
-with `s1` as the first new intermediate state"
+      Falling back to the default numbering schema,
+      with `s1` as the first new intermediate state"
     modifyThe SymContext ({ · with
       state_prefix := "s",
       currentStateNumber := 1 })

diff --git a/lakefile.lean b/lakefile.lean
@@ -32,9 +32,6 @@ lean_lib «Tactics» where
 lean_lib «Doc» where
   -- add library configuration options here
 
-lean_lib «Benchmarks» where
-  -- add library configuration options here
-
 @[default_target]
 lean_exe «lnsym» where
   root := `Main