Automate the generation of the lakefile.lean files

1 files changed, 3 insertions, 7 deletions

diff --git a/tests/lean/hashmap_on_disk/lakefile.lean b/tests/lean/hashmap_on_disk/lakefile.lean
index 0ca1ef9b..bdb614cd 100644
--- a/tests/lean/hashmap_on_disk/lakefile.lean
+++ b/tests/lean/hashmap_on_disk/lakefile.lean
@@ -4,19 +4,15 @@ open Lake DSL
 require mathlib from git
   "https://github.com/leanprover-community/mathlib4.git"
 
-package «hashmap» {
+package «hashmap_main» {
   -- add package configuration options here
 }
 
-lean_lib «HashmapMain» {
+lean_lib «Base» {
   -- add library configuration options here
 }
 
-lean_lib «Base» {
+lean_lib «HashmapMain» {
   -- add library configuration options here
 }
 
-@[default_target]
-lean_exe «hashmap» {
-  root := `Main
-}