summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2023-03-07 17:49:03 +0100
committerSon HO2023-06-04 21:44:33 +0200
commit4db56fe2c963a4052f8415b3985c8765407fccbc (patch)
tree53c5f05469bb3946547c418176f35d840dbe6012
parent051e2a19f3268d272a0acd0425d2107ebea020c5 (diff)
Update the extraction of Lean files
-rw-r--r--compiler/Extract.ml42
-rw-r--r--compiler/Translate.ml34
-rw-r--r--tests/lean/.gitignore2
-rw-r--r--tests/lean/Makefile40
-rw-r--r--tests/lean/betree/BetreeMain.lean1
-rw-r--r--tests/lean/betree/BetreeMain/Types.lean18
-rw-r--r--tests/lean/betree/lake-manifest.json27
-rw-r--r--tests/lean/betree/lakefile.lean14
-rw-r--r--tests/lean/betree/lean-toolchain1
-rw-r--r--tests/lean/hashmap/Hashmap.lean1
-rw-r--r--tests/lean/hashmap/Hashmap/Types.lean2
-rw-r--r--tests/lean/hashmap/lake-manifest.json27
-rw-r--r--tests/lean/hashmap/lakefile.lean14
-rw-r--r--tests/lean/hashmap/lean-toolchain1
-rw-r--r--tests/lean/hashmap_on_disk/HashmapMain.lean2
-rw-r--r--tests/lean/hashmap_on_disk/HashmapMain/Clauses/Clauses.lean18
-rw-r--r--tests/lean/hashmap_on_disk/HashmapMain/Funs.lean23
-rw-r--r--tests/lean/hashmap_on_disk/HashmapMain/Types.lean4
-rw-r--r--tests/lean/hashmap_on_disk/lake-manifest.json8
-rw-r--r--tests/lean/hashmap_on_disk/lakefile.lean14
-rw-r--r--tests/lean/lean-toolchain1
-rw-r--r--tests/lean/misc-constants/Constants.lean7
-rw-r--r--tests/lean/misc-constants/lake-manifest.json27
-rw-r--r--tests/lean/misc-constants/lakefile.lean14
-rw-r--r--tests/lean/misc-constants/lean-toolchain1
-rw-r--r--tests/lean/misc-external/External.lean1
-rw-r--r--tests/lean/misc-external/External/Types.lean4
-rw-r--r--tests/lean/misc-external/lake-manifest.json27
-rw-r--r--tests/lean/misc-external/lakefile.lean14
-rw-r--r--tests/lean/misc-external/lean-toolchain1
-rw-r--r--tests/lean/misc-loops/Loops.lean1
-rw-r--r--tests/lean/misc-loops/lake-manifest.json27
-rw-r--r--tests/lean/misc-loops/lakefile.lean14
-rw-r--r--tests/lean/misc-loops/lean-toolchain1
-rw-r--r--tests/lean/misc-no_nested_borrows/NoNestedBorrows.lean20
-rw-r--r--tests/lean/misc-no_nested_borrows/lake-manifest.json27
-rw-r--r--tests/lean/misc-no_nested_borrows/lakefile.lean14
-rw-r--r--tests/lean/misc-no_nested_borrows/lean-toolchain1
-rw-r--r--tests/lean/misc-paper/lake-manifest.json27
-rw-r--r--tests/lean/misc-paper/lakefile.lean14
-rw-r--r--tests/lean/misc-paper/lean-toolchain1
-rw-r--r--tests/lean/misc-polonius_list/lake-manifest.json27
-rw-r--r--tests/lean/misc-polonius_list/lakefile.lean14
-rw-r--r--tests/lean/misc-polonius_list/lean-toolchain1
44 files changed, 415 insertions, 164 deletions
diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index 63d41d9a..0b8d8bdf 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -973,8 +973,9 @@ let extract_type_decl_struct_body (ctx : extraction_ctx) (fmt : F.formatter)
if !backend = FStar && fields = [] then (
F.pp_print_space fmt ();
F.pp_print_string fmt (unit_name ()))
+ else if !backend = Lean && fields = [] then ()
else if (not is_rec) || !backend <> Coq then (
- F.pp_print_space fmt ();
+ if !backend <> Lean then F.pp_print_space fmt ();
(* If Coq: print the constructor name *)
(* TODO: remove superfluous test not is_rec below *)
if !backend = Coq && not is_rec then (
@@ -985,10 +986,14 @@ let extract_type_decl_struct_body (ctx : extraction_ctx) (fmt : F.formatter)
if !backend <> Lean then F.pp_print_string fmt "{";
F.pp_print_break fmt 1 ctx.indent_incr;
(* The body itself *)
- F.pp_open_hvbox fmt 0;
+ (* Open a box for the body *)
+ (match !backend with
+ | Coq | FStar -> F.pp_open_hvbox fmt 0
+ | Lean -> F.pp_open_vbox fmt 0);
(* Print the fields *)
let print_field (field_id : FieldId.id) (f : field) : unit =
let field_name = ctx_get_field (AdtId def.def_id) field_id ctx in
+ (* Open a box for the field *)
F.pp_open_box fmt ctx.indent_incr;
F.pp_print_string fmt field_name;
F.pp_print_space fmt ();
@@ -996,20 +1001,21 @@ let extract_type_decl_struct_body (ctx : extraction_ctx) (fmt : F.formatter)
F.pp_print_space fmt ();
extract_ty ctx fmt false f.field_ty;
if !backend <> Lean then F.pp_print_string fmt ";";
+ (* Close the box for the field *)
F.pp_close_box fmt ()
in
let fields = FieldId.mapi (fun fid f -> (fid, f)) fields in
Collections.List.iter_link (F.pp_print_space fmt)
(fun (fid, f) -> print_field fid f)
fields;
- (* Close *)
+ (* Close the box for the body *)
F.pp_close_box fmt ();
- F.pp_print_space fmt ();
- if !backend <> Lean then F.pp_print_string fmt "}")
+ if !backend <> Lean then (
+ F.pp_print_space fmt ();
+ F.pp_print_string fmt "}"))
else (
(* We extract for Coq, and we have a recursive record, or a record in
- a group of mutually recursive types: we extract it as an inductive type
- *)
+ a group of mutually recursive types: we extract it as an inductive type *)
assert (is_rec && !backend = Coq);
let with_opaque_pre = false in
let cons_name = ctx_get_struct with_opaque_pre (AdtId def.def_id) ctx in
@@ -1068,10 +1074,13 @@ let extract_type_decl (ctx : extraction_ctx) (fmt : F.formatter)
F.pp_print_break fmt 0 0;
(* Print a comment to link the extracted type to its original rust definition *)
extract_comment fmt ("[" ^ Print.name_to_string def.name ^ "]");
- F.pp_print_space fmt ();
+ F.pp_print_break fmt 0 0;
(* Open a box for the definition, so that whenever possible it gets printed on
- * one line *)
- F.pp_open_hvbox fmt 0;
+ * one line. Note however that in the case of Lean line breaks are important
+ * for parsing: we thus use a hovbox. *)
+ (match !backend with
+ | Coq | FStar -> F.pp_open_hvbox fmt 0
+ | Lean -> F.pp_open_vbox fmt 0);
(* Open a box for "type TYPE_NAME (TYPE_PARAMS) =" *)
F.pp_open_hovbox fmt ctx.indent_incr;
(* > "type TYPE_NAME" *)
@@ -1111,7 +1120,7 @@ let extract_type_decl (ctx : extraction_ctx) (fmt : F.formatter)
in
F.pp_print_string fmt eq)
else (
- (* Otherwise print ": Type0" *)
+ (* Otherwise print ": Type" *)
if use_forall then F.pp_print_string fmt ","
else (
F.pp_print_space fmt ();
@@ -1384,7 +1393,7 @@ let extract_state_type (fmt : F.formatter) (ctx : extraction_ctx)
F.pp_print_break fmt 0 0;
(* Print a comment *)
extract_comment fmt "The state type used in the state-error monad";
- F.pp_print_space fmt ();
+ F.pp_print_break fmt 0 0;
(* Open a box for the definition, so that whenever possible it gets printed on
* one line *)
F.pp_open_hvbox fmt 0;
@@ -1392,8 +1401,13 @@ let extract_state_type (fmt : F.formatter) (ctx : extraction_ctx)
let state_name = ctx_get_assumed_type State ctx in
(* The syntax for Lean and Coq is almost identical. *)
let print_axiom () =
- if !backend = Coq then F.pp_print_string fmt "Axiom"
- else F.pp_print_string fmt "axiom";
+ let axiom =
+ match !backend with
+ | Coq -> "Axiom"
+ | Lean -> "axiom"
+ | FStar -> raise (Failure "Unexpected")
+ in
+ F.pp_print_string fmt axiom;
F.pp_print_space fmt ();
F.pp_print_string fmt state_name;
F.pp_print_space fmt ();
diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index ab1addab..3278aa6a 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -679,18 +679,20 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config)
of the functions marked as Opaque. We emit the `structure ...` bit here,
then rely on `extract_fun_decl` to be aware of this, and skip the keyword
(e.g. "axiom" or "val") so as to generate valid syntax for records. *)
- if config.extract_opaque && config.extract_fun_decls && !Config.backend = Lean
- then (
+ let wrap_in_sig =
+ config.extract_opaque && config.extract_fun_decls && !Config.backend = Lean
+ in
+ if wrap_in_sig then (
Format.pp_print_break fmt 0 0;
Format.pp_open_vbox fmt ctx.extract_ctx.indent_incr;
Format.pp_print_string fmt "structure OpaqueDefs where";
Format.pp_print_break fmt 0 0);
List.iter export_decl_group ctx.crate.declarations;
- if config.extract_opaque && !Config.backend = Lean then
- Format.pp_close_box fmt ();
if config.extract_state_type && not config.extract_fun_decls then
- export_state_type ()
+ export_state_type ();
+
+ if wrap_in_sig then Format.pp_close_box fmt ()
let extract_file (config : gen_config) (ctx : gen_ctx) (filename : string)
(rust_module_name : string) (module_name : string) (custom_msg : string)
@@ -1117,6 +1119,19 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
*)
| Lean ->
(*
+ * Generate the library entry point, if the crate is split between
+ * different files.
+ *)
+ if !Config.split_files then (
+ let filename = Filename.concat dest_dir (module_name ^ ".lean") in
+ let out = open_out filename in
+ (* Write *)
+ Printf.fprintf out "import %s.Funs\n" module_name;
+ (* Flush and close the file, log *)
+ close_out out;
+ log#linfo (lazy ("Generated: " ^ filename)));
+
+ (*
* Generate the lakefile.lean file
*)
@@ -1131,14 +1146,11 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
" \"https://github.com/leanprover-community/mathlib4.git\"\n\n";
let package_name = StringUtils.to_snake_case module_name in
- Printf.fprintf out "package «%s» {\n" package_name;
- Printf.fprintf out " -- add package configuration options here\n}\n\n";
+ Printf.fprintf out "package «%s» {}\n\n" package_name;
- Printf.fprintf out "lean_lib «Base» {\n";
- Printf.fprintf out " -- add library configuration options here\n}\n\n";
+ Printf.fprintf out "lean_lib «Base» {}\n\n";
- Printf.fprintf out "lean_lib «%s» {\n" module_name;
- Printf.fprintf out " -- add library configuration options here\n}\n\n";
+ Printf.fprintf out "@[default_target]\nlean_lib «%s» {}\n" module_name;
(* No default target for now.
Format would be:
diff --git a/tests/lean/.gitignore b/tests/lean/.gitignore
new file mode 100644
index 00000000..e74f9899
--- /dev/null
+++ b/tests/lean/.gitignore
@@ -0,0 +1,2 @@
+*/lake-packages/
+*/build/ \ No newline at end of file
diff --git a/tests/lean/Makefile b/tests/lean/Makefile
new file mode 100644
index 00000000..ed3b3e3b
--- /dev/null
+++ b/tests/lean/Makefile
@@ -0,0 +1,40 @@
+ALL_DIRS ?= $(filter-out %~ lean-toolchain% Makefile%, $(wildcard *))
+
+UPDATE_DIRS = $(addprefix update-,$(ALL_DIRS))
+
+VERIFY_DIRS = $(addprefix verif-,$(ALL_DIRS))
+
+CLEAN_DIRS = $(addprefix clean-,$(ALL_DIRS))
+
+COPY_LEAN_TOOLCHAIN = $(addprefix copy-lean-toolchain-,$(ALL_DIRS))
+
+.PHONY: all
+all: prepare-projects verify
+
+.PHONY: prepare-projects
+prepare-projects: $(COPY_LEAN_TOOLCHAIN)
+
+.PHONY: prepare-projects
+copy-lean-toolchain-%:
+ cp lean-toolchain $*
+
+.PHONY: update
+update: $(UPDATE_DIRS)
+
+.PHONY: update-%
+update-%:
+ cd $* && lake update
+
+.PHONY: verify
+verify: $(VERIFY_DIRS)
+
+.PHONY: verif-%
+verif-%:
+ cd $* && lake build
+
+.PHONY: clean
+clean: $(CLEAN_DIRS)
+
+.PHONY: clean-%
+clean-%:
+ cd $* && lake clean
diff --git a/tests/lean/betree/BetreeMain.lean b/tests/lean/betree/BetreeMain.lean
new file mode 100644
index 00000000..5f307877
--- /dev/null
+++ b/tests/lean/betree/BetreeMain.lean
@@ -0,0 +1 @@
+import BetreeMain.Funs
diff --git a/tests/lean/betree/BetreeMain/Types.lean b/tests/lean/betree/BetreeMain/Types.lean
index 2726e1f0..e2e6c867 100644
--- a/tests/lean/betree/BetreeMain/Types.lean
+++ b/tests/lean/betree/BetreeMain/Types.lean
@@ -20,9 +20,8 @@ inductive betree_message_t :=
/- [betree_main::betree::Leaf] -/
structure betree_leaf_t where
-
- betree_leaf_id : UInt64 betree_leaf_size : UInt64
-
+ betree_leaf_id : UInt64
+ betree_leaf_size : UInt64
/- [betree_main::betree::Node] -/
mutual inductive betree_node_t :=
@@ -31,31 +30,26 @@ mutual inductive betree_node_t :=
/- [betree_main::betree::Internal] -/
inductive betree_internal_t :=
-
betree_internal_id : UInt64
betree_internal_pivot : UInt64
betree_internal_left : betree_node_t
betree_internal_right : betree_node_t
-
/- [betree_main::betree::Params] -/
structure betree_params_t where
-
- betree_params_min_flush_size : UInt64 betree_params_split_size : UInt64
-
+ betree_params_min_flush_size : UInt64
+ betree_params_split_size : UInt64
/- [betree_main::betree::NodeIdCounter] -/
structure betree_node_id_counter_t where
-
betree_node_id_counter_next_node_id : UInt64
-
/- [betree_main::betree::BeTree] -/
structure betree_be_tree_t where
-
betree_be_tree_params : betree_params_t
betree_be_tree_node_id_cnt : betree_node_id_counter_t
betree_be_tree_root : betree_node_t
-/- The state type used in the state-error monad -/ axiom State : Type
+/- The state type used in the state-error monad -/
+axiom State : Type
diff --git a/tests/lean/betree/lake-manifest.json b/tests/lean/betree/lake-manifest.json
new file mode 100644
index 00000000..57b071ca
--- /dev/null
+++ b/tests/lean/betree/lake-manifest.json
@@ -0,0 +1,27 @@
+{"version": 4,
+ "packagesDir": "./lake-packages",
+ "packages":
+ [{"git":
+ {"url": "https://github.com/leanprover-community/mathlib4.git",
+ "subDir?": null,
+ "rev": "4037792ead804d7bfa8868e2c4684d4223c15ece",
+ "name": "mathlib",
+ "inputRev?": null}},
+ {"git":
+ {"url": "https://github.com/gebner/quote4",
+ "subDir?": null,
+ "rev": "2412c4fdf4a8b689f4467618e5e7b371ae5014aa",
+ "name": "Qq",
+ "inputRev?": "master"}},
+ {"git":
+ {"url": "https://github.com/JLimperg/aesop",
+ "subDir?": null,
+ "rev": "7fe9ecd9339b0e1796e89d243b776849c305c690",
+ "name": "aesop",
+ "inputRev?": "master"}},
+ {"git":
+ {"url": "https://github.com/leanprover/std4",
+ "subDir?": null,
+ "rev": "24897887905b3a1254b244369f5dd2cf6174b0ee",
+ "name": "std",
+ "inputRev?": "main"}}]}
diff --git a/tests/lean/betree/lakefile.lean b/tests/lean/betree/lakefile.lean
index aa702300..ac2cc2d8 100644
--- a/tests/lean/betree/lakefile.lean
+++ b/tests/lean/betree/lakefile.lean
@@ -4,15 +4,9 @@ open Lake DSL
require mathlib from git
"https://github.com/leanprover-community/mathlib4.git"
-package «betree_main» {
- -- add package configuration options here
-}
+package «betree_main» {}
-lean_lib «Base» {
- -- add library configuration options here
-}
-
-lean_lib «BetreeMain» {
- -- add library configuration options here
-}
+lean_lib «Base» {}
+@[default_target]
+lean_lib «BetreeMain» {}
diff --git a/tests/lean/betree/lean-toolchain b/tests/lean/betree/lean-toolchain
new file mode 100644
index 00000000..bbf57f10
--- /dev/null
+++ b/tests/lean/betree/lean-toolchain
@@ -0,0 +1 @@
+leanprover/lean4:nightly-2023-01-21
diff --git a/tests/lean/hashmap/Hashmap.lean b/tests/lean/hashmap/Hashmap.lean
new file mode 100644
index 00000000..41630205
--- /dev/null
+++ b/tests/lean/hashmap/Hashmap.lean
@@ -0,0 +1 @@
+import Hashmap.Funs
diff --git a/tests/lean/hashmap/Hashmap/Types.lean b/tests/lean/hashmap/Hashmap/Types.lean
index 750bf6de..dd2be633 100644
--- a/tests/lean/hashmap/Hashmap/Types.lean
+++ b/tests/lean/hashmap/Hashmap/Types.lean
@@ -9,10 +9,8 @@ inductive list_t (T : Type) :=
/- [hashmap::HashMap] -/
structure hash_map_t (T : Type) where
-
hash_map_num_entries : USize
hash_map_max_load_factor : (USize × USize)
hash_map_max_load : USize
hash_map_slots : Vec (list_t T)
-
diff --git a/tests/lean/hashmap/lake-manifest.json b/tests/lean/hashmap/lake-manifest.json
new file mode 100644
index 00000000..57b071ca
--- /dev/null
+++ b/tests/lean/hashmap/lake-manifest.json
@@ -0,0 +1,27 @@
+{"version": 4,
+ "packagesDir": "./lake-packages",
+ "packages":
+ [{"git":
+ {"url": "https://github.com/leanprover-community/mathlib4.git",
+ "subDir?": null,
+ "rev": "4037792ead804d7bfa8868e2c4684d4223c15ece",
+ "name": "mathlib",
+ "inputRev?": null}},
+ {"git":
+ {"url": "https://github.com/gebner/quote4",
+ "subDir?": null,
+ "rev": "2412c4fdf4a8b689f4467618e5e7b371ae5014aa",
+ "name": "Qq",
+ "inputRev?": "master"}},
+ {"git":
+ {"url": "https://github.com/JLimperg/aesop",
+ "subDir?": null,
+ "rev": "7fe9ecd9339b0e1796e89d243b776849c305c690",
+ "name": "aesop",
+ "inputRev?": "master"}},
+ {"git":
+ {"url": "https://github.com/leanprover/std4",
+ "subDir?": null,
+ "rev": "24897887905b3a1254b244369f5dd2cf6174b0ee",
+ "name": "std",
+ "inputRev?": "main"}}]}
diff --git a/tests/lean/hashmap/lakefile.lean b/tests/lean/hashmap/lakefile.lean
index c7d79306..713785f6 100644
--- a/tests/lean/hashmap/lakefile.lean
+++ b/tests/lean/hashmap/lakefile.lean
@@ -4,15 +4,9 @@ open Lake DSL
require mathlib from git
"https://github.com/leanprover-community/mathlib4.git"
-package «hashmap» {
- -- add package configuration options here
-}
+package «hashmap» {}
-lean_lib «Base» {
- -- add library configuration options here
-}
-
-lean_lib «Hashmap» {
- -- add library configuration options here
-}
+lean_lib «Base» {}
+@[default_target]
+lean_lib «Hashmap» {}
diff --git a/tests/lean/hashmap/lean-toolchain b/tests/lean/hashmap/lean-toolchain
new file mode 100644
index 00000000..bbf57f10
--- /dev/null
+++ b/tests/lean/hashmap/lean-toolchain
@@ -0,0 +1 @@
+leanprover/lean4:nightly-2023-01-21
diff --git a/tests/lean/hashmap_on_disk/HashmapMain.lean b/tests/lean/hashmap_on_disk/HashmapMain.lean
index 99415d9d..1a4e7f82 100644
--- a/tests/lean/hashmap_on_disk/HashmapMain.lean
+++ b/tests/lean/hashmap_on_disk/HashmapMain.lean
@@ -1 +1 @@
-def hello := "world"
+import HashmapMain.Funs
diff --git a/tests/lean/hashmap_on_disk/HashmapMain/Clauses/Clauses.lean b/tests/lean/hashmap_on_disk/HashmapMain/Clauses/Clauses.lean
index 16a4ea4c..a514c58a 100644
--- a/tests/lean/hashmap_on_disk/HashmapMain/Clauses/Clauses.lean
+++ b/tests/lean/hashmap_on_disk/HashmapMain/Clauses/Clauses.lean
@@ -1,11 +1,12 @@
--- [hashmap_main]: decreases clauses
+-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
+-- [hashmap_main]: templates for the decreases clauses
import Base.Primitives
import HashmapMain.Types
/- [hashmap_main::hashmap::HashMap::{0}::allocate_slots]: termination measure -/
@[simp]
def hashmap_hash_map_allocate_slots_loop_terminates (T : Type)
- (slots : vec (hashmap_list_t T)) (n : USize) :=
+ (slots : Vec (hashmap_list_t T)) (n : USize) :=
(slots, n)
syntax "hashmap_hash_map_allocate_slots_loop_decreases" term+ : tactic
@@ -14,16 +15,17 @@ macro_rules
| `(tactic| hashmap_hash_map_allocate_slots_loop_decreases $slots $n) =>
`(tactic| sorry)
-/- [hashmap_main::hashmap::HashMap::{0}::clear]: termination measure -/
+/- [hashmap_main::hashmap::HashMap::{0}::clear_slots]: termination measure -/
@[simp]
-def hashmap_hash_map_clear_loop_terminates (T : Type)
- (slots : vec (hashmap_list_t T)) (i : USize) :=
+def hashmap_hash_map_clear_slots_loop_terminates (T : Type)
+ (slots : Vec (hashmap_list_t T)) (i : USize) :=
(slots, i)
-syntax "hashmap_hash_map_clear_loop_decreases" term+ : tactic
+syntax "hashmap_hash_map_clear_slots_loop_decreases" term+ : tactic
macro_rules
-| `(tactic| hashmap_hash_map_clear_loop_decreases $slots $i) =>`(tactic| sorry)
+| `(tactic| hashmap_hash_map_clear_slots_loop_decreases $slots $i) =>
+ `(tactic| sorry)
/- [hashmap_main::hashmap::HashMap::{0}::insert_in_list]: termination measure -/
@[simp]
@@ -52,7 +54,7 @@ $ls) =>`(tactic| sorry)
/- [hashmap_main::hashmap::HashMap::{0}::move_elements]: termination measure -/
@[simp]
def hashmap_hash_map_move_elements_loop_terminates (T : Type)
- (ntable : hashmap_hash_map_t T) (slots : vec (hashmap_list_t T)) (i : USize)
+ (ntable : hashmap_hash_map_t T) (slots : Vec (hashmap_list_t T)) (i : USize)
:=
(ntable, slots, i)
diff --git a/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean b/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean
index c85d14f4..392c8816 100644
--- a/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean
+++ b/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean
@@ -60,8 +60,8 @@ def hashmap_hash_map_new_fwd (T : Type) : Result (hashmap_hash_map_t T) :=
hashmap_hash_map_new_with_capacity_fwd T (USize.ofNatCore 32 (by intlit))
(USize.ofNatCore 4 (by intlit)) (USize.ofNatCore 5 (by intlit))
-/- [hashmap_main::hashmap::HashMap::{0}::clear] -/
-def hashmap_hash_map_clear_loop_fwd_back
+/- [hashmap_main::hashmap::HashMap::{0}::clear_slots] -/
+def hashmap_hash_map_clear_slots_loop_fwd_back
(T : Type) (slots : Vec (hashmap_list_t T)) (i : USize) :
(Result (Vec (hashmap_list_t T)))
:=
@@ -73,19 +73,26 @@ def hashmap_hash_map_clear_loop_fwd_back
let slots0 ←
vec_index_mut_back (hashmap_list_t T) slots i
hashmap_list_t.HashmapListNil
- hashmap_hash_map_clear_loop_fwd_back T slots0 i1
+ hashmap_hash_map_clear_slots_loop_fwd_back T slots0 i1
else Result.ret slots
-termination_by hashmap_hash_map_clear_loop_fwd_back slots i =>
- hashmap_hash_map_clear_loop_terminates T slots i
-decreasing_by hashmap_hash_map_clear_loop_decreases slots i
+termination_by hashmap_hash_map_clear_slots_loop_fwd_back slots i =>
+ hashmap_hash_map_clear_slots_loop_terminates T slots i
+decreasing_by hashmap_hash_map_clear_slots_loop_decreases slots i
+
+/- [hashmap_main::hashmap::HashMap::{0}::clear_slots] -/
+def hashmap_hash_map_clear_slots_fwd_back
+ (T : Type) (slots : Vec (hashmap_list_t T)) :
+ Result (Vec (hashmap_list_t T))
+ :=
+ hashmap_hash_map_clear_slots_loop_fwd_back T slots
+ (USize.ofNatCore 0 (by intlit))
/- [hashmap_main::hashmap::HashMap::{0}::clear] -/
def hashmap_hash_map_clear_fwd_back
(T : Type) (self : hashmap_hash_map_t T) : Result (hashmap_hash_map_t T) :=
do
let v ←
- hashmap_hash_map_clear_loop_fwd_back T self.hashmap_hash_map_slots
- (USize.ofNatCore 0 (by intlit))
+ hashmap_hash_map_clear_slots_fwd_back T self.hashmap_hash_map_slots
Result.ret
{
hashmap_hash_map_num_entries := (USize.ofNatCore 0 (by intlit)),
diff --git a/tests/lean/hashmap_on_disk/HashmapMain/Types.lean b/tests/lean/hashmap_on_disk/HashmapMain/Types.lean
index 40f9b7e9..fbab1bcd 100644
--- a/tests/lean/hashmap_on_disk/HashmapMain/Types.lean
+++ b/tests/lean/hashmap_on_disk/HashmapMain/Types.lean
@@ -9,11 +9,11 @@ inductive hashmap_list_t (T : Type) :=
/- [hashmap_main::hashmap::HashMap] -/
structure hashmap_hash_map_t (T : Type) where
-
hashmap_hash_map_num_entries : USize
hashmap_hash_map_max_load_factor : (USize × USize)
hashmap_hash_map_max_load : USize
hashmap_hash_map_slots : Vec (hashmap_list_t T)
-/- The state type used in the state-error monad -/ axiom State : Type
+/- The state type used in the state-error monad -/
+axiom State : Type
diff --git a/tests/lean/hashmap_on_disk/lake-manifest.json b/tests/lean/hashmap_on_disk/lake-manifest.json
index 8ac53836..57b071ca 100644
--- a/tests/lean/hashmap_on_disk/lake-manifest.json
+++ b/tests/lean/hashmap_on_disk/lake-manifest.json
@@ -4,24 +4,24 @@
[{"git":
{"url": "https://github.com/leanprover-community/mathlib4.git",
"subDir?": null,
- "rev": "583f6cfa4bced545c797216b32600d6211b753f9",
+ "rev": "4037792ead804d7bfa8868e2c4684d4223c15ece",
"name": "mathlib",
"inputRev?": null}},
{"git":
{"url": "https://github.com/gebner/quote4",
"subDir?": null,
- "rev": "7ac99aa3fac487bec1d5860e751b99c7418298cf",
+ "rev": "2412c4fdf4a8b689f4467618e5e7b371ae5014aa",
"name": "Qq",
"inputRev?": "master"}},
{"git":
{"url": "https://github.com/JLimperg/aesop",
"subDir?": null,
- "rev": "ccff5d4ae7411c5fe741f3139950e8bddf353dea",
+ "rev": "7fe9ecd9339b0e1796e89d243b776849c305c690",
"name": "aesop",
"inputRev?": "master"}},
{"git":
{"url": "https://github.com/leanprover/std4",
"subDir?": null,
- "rev": "cda27d551340756d5ed6f9b83716a9db799c5537",
+ "rev": "24897887905b3a1254b244369f5dd2cf6174b0ee",
"name": "std",
"inputRev?": "main"}}]}
diff --git a/tests/lean/hashmap_on_disk/lakefile.lean b/tests/lean/hashmap_on_disk/lakefile.lean
index bdb614cd..70daf427 100644
--- a/tests/lean/hashmap_on_disk/lakefile.lean
+++ b/tests/lean/hashmap_on_disk/lakefile.lean
@@ -4,15 +4,9 @@ open Lake DSL
require mathlib from git
"https://github.com/leanprover-community/mathlib4.git"
-package «hashmap_main» {
- -- add package configuration options here
-}
+package «hashmap_main» {}
-lean_lib «Base» {
- -- add library configuration options here
-}
-
-lean_lib «HashmapMain» {
- -- add library configuration options here
-}
+lean_lib «Base» {}
+@[default_target]
+lean_lib «HashmapMain» {}
diff --git a/tests/lean/lean-toolchain b/tests/lean/lean-toolchain
new file mode 100644
index 00000000..bbf57f10
--- /dev/null
+++ b/tests/lean/lean-toolchain
@@ -0,0 +1 @@
+leanprover/lean4:nightly-2023-01-21
diff --git a/tests/lean/misc-constants/Constants.lean b/tests/lean/misc-constants/Constants.lean
index 57f6e403..937a15e5 100644
--- a/tests/lean/misc-constants/Constants.lean
+++ b/tests/lean/misc-constants/Constants.lean
@@ -35,7 +35,9 @@ structure OpaqueDefs where
Result.ret (x, y)
/- [constants::Pair] -/
- structure pair_t (T1 T2 : Type) where pair_x : T1 pair_y : T2
+ structure pair_t (T1 T2 : Type) where
+ pair_x : T1
+ pair_y : T2
/- [constants::mk_pair1] -/
def mk_pair1_fwd (x : UInt32) (y : UInt32) : Result (pair_t UInt32 UInt32) :=
@@ -70,7 +72,8 @@ structure OpaqueDefs where
def p3_c : pair_t UInt32 UInt32 := eval_global p3_body (by simp)
/- [constants::Wrap] -/
- structure wrap_t (T : Type) where wrap_val : T
+ structure wrap_t (T : Type) where
+ wrap_val : T
/- [constants::Wrap::{0}::new] -/
def wrap_new_fwd (T : Type) (val : T) : Result (wrap_t T) :=
diff --git a/tests/lean/misc-constants/lake-manifest.json b/tests/lean/misc-constants/lake-manifest.json
new file mode 100644
index 00000000..57b071ca
--- /dev/null
+++ b/tests/lean/misc-constants/lake-manifest.json
@@ -0,0 +1,27 @@
+{"version": 4,
+ "packagesDir": "./lake-packages",
+ "packages":
+ [{"git":
+ {"url": "https://github.com/leanprover-community/mathlib4.git",
+ "subDir?": null,
+ "rev": "4037792ead804d7bfa8868e2c4684d4223c15ece",
+ "name": "mathlib",
+ "inputRev?": null}},
+ {"git":
+ {"url": "https://github.com/gebner/quote4",
+ "subDir?": null,
+ "rev": "2412c4fdf4a8b689f4467618e5e7b371ae5014aa",
+ "name": "Qq",
+ "inputRev?": "master"}},
+ {"git":
+ {"url": "https://github.com/JLimperg/aesop",
+ "subDir?": null,
+ "rev": "7fe9ecd9339b0e1796e89d243b776849c305c690",
+ "name": "aesop",
+ "inputRev?": "master"}},
+ {"git":
+ {"url": "https://github.com/leanprover/std4",
+ "subDir?": null,
+ "rev": "24897887905b3a1254b244369f5dd2cf6174b0ee",
+ "name": "std",
+ "inputRev?": "main"}}]}
diff --git a/tests/lean/misc-constants/lakefile.lean b/tests/lean/misc-constants/lakefile.lean
index ed8eebc2..01aacb90 100644
--- a/tests/lean/misc-constants/lakefile.lean
+++ b/tests/lean/misc-constants/lakefile.lean
@@ -4,15 +4,9 @@ open Lake DSL
require mathlib from git
"https://github.com/leanprover-community/mathlib4.git"
-package «constants» {
- -- add package configuration options here
-}
+package «constants» {}
-lean_lib «Base» {
- -- add library configuration options here
-}
-
-lean_lib «Constants» {
- -- add library configuration options here
-}
+lean_lib «Base» {}
+@[default_target]
+lean_lib «Constants» {}
diff --git a/tests/lean/misc-constants/lean-toolchain b/tests/lean/misc-constants/lean-toolchain
new file mode 100644
index 00000000..bbf57f10
--- /dev/null
+++ b/tests/lean/misc-constants/lean-toolchain
@@ -0,0 +1 @@
+leanprover/lean4:nightly-2023-01-21
diff --git a/tests/lean/misc-external/External.lean b/tests/lean/misc-external/External.lean
new file mode 100644
index 00000000..b95db309
--- /dev/null
+++ b/tests/lean/misc-external/External.lean
@@ -0,0 +1 @@
+import External.Funs
diff --git a/tests/lean/misc-external/External/Types.lean b/tests/lean/misc-external/External/Types.lean
index 386832f4..ed1842be 100644
--- a/tests/lean/misc-external/External/Types.lean
+++ b/tests/lean/misc-external/External/Types.lean
@@ -4,5 +4,7 @@ import Base.Primitives
/- [core::num::nonzero::NonZeroU32] -/
axiom core_num_nonzero_non_zero_u32_t : Type
-/- The state type used in the state-error monad -/ axiom State : Type
+
+/- The state type used in the state-error monad -/
+axiom State : Type
diff --git a/tests/lean/misc-external/lake-manifest.json b/tests/lean/misc-external/lake-manifest.json
new file mode 100644
index 00000000..57b071ca
--- /dev/null
+++ b/tests/lean/misc-external/lake-manifest.json
@@ -0,0 +1,27 @@
+{"version": 4,
+ "packagesDir": "./lake-packages",
+ "packages":
+ [{"git":
+ {"url": "https://github.com/leanprover-community/mathlib4.git",
+ "subDir?": null,
+ "rev": "4037792ead804d7bfa8868e2c4684d4223c15ece",
+ "name": "mathlib",
+ "inputRev?": null}},
+ {"git":
+ {"url": "https://github.com/gebner/quote4",
+ "subDir?": null,
+ "rev": "2412c4fdf4a8b689f4467618e5e7b371ae5014aa",
+ "name": "Qq",
+ "inputRev?": "master"}},
+ {"git":
+ {"url": "https://github.com/JLimperg/aesop",
+ "subDir?": null,
+ "rev": "7fe9ecd9339b0e1796e89d243b776849c305c690",
+ "name": "aesop",
+ "inputRev?": "master"}},
+ {"git":
+ {"url": "https://github.com/leanprover/std4",
+ "subDir?": null,
+ "rev": "24897887905b3a1254b244369f5dd2cf6174b0ee",
+ "name": "std",
+ "inputRev?": "main"}}]}
diff --git a/tests/lean/misc-external/lakefile.lean b/tests/lean/misc-external/lakefile.lean
index b883f4b9..6cc4aae4 100644
--- a/tests/lean/misc-external/lakefile.lean
+++ b/tests/lean/misc-external/lakefile.lean
@@ -4,15 +4,9 @@ open Lake DSL
require mathlib from git
"https://github.com/leanprover-community/mathlib4.git"
-package «external» {
- -- add package configuration options here
-}
+package «external» {}
-lean_lib «Base» {
- -- add library configuration options here
-}
-
-lean_lib «External» {
- -- add library configuration options here
-}
+lean_lib «Base» {}
+@[default_target]
+lean_lib «External» {}
diff --git a/tests/lean/misc-external/lean-toolchain b/tests/lean/misc-external/lean-toolchain
new file mode 100644
index 00000000..bbf57f10
--- /dev/null
+++ b/tests/lean/misc-external/lean-toolchain
@@ -0,0 +1 @@
+leanprover/lean4:nightly-2023-01-21
diff --git a/tests/lean/misc-loops/Loops.lean b/tests/lean/misc-loops/Loops.lean
new file mode 100644
index 00000000..60c73776
--- /dev/null
+++ b/tests/lean/misc-loops/Loops.lean
@@ -0,0 +1 @@
+import Loops.Funs
diff --git a/tests/lean/misc-loops/lake-manifest.json b/tests/lean/misc-loops/lake-manifest.json
new file mode 100644
index 00000000..57b071ca
--- /dev/null
+++ b/tests/lean/misc-loops/lake-manifest.json
@@ -0,0 +1,27 @@
+{"version": 4,
+ "packagesDir": "./lake-packages",
+ "packages":
+ [{"git":
+ {"url": "https://github.com/leanprover-community/mathlib4.git",
+ "subDir?": null,
+ "rev": "4037792ead804d7bfa8868e2c4684d4223c15ece",
+ "name": "mathlib",
+ "inputRev?": null}},
+ {"git":
+ {"url": "https://github.com/gebner/quote4",
+ "subDir?": null,
+ "rev": "2412c4fdf4a8b689f4467618e5e7b371ae5014aa",
+ "name": "Qq",
+ "inputRev?": "master"}},
+ {"git":
+ {"url": "https://github.com/JLimperg/aesop",
+ "subDir?": null,
+ "rev": "7fe9ecd9339b0e1796e89d243b776849c305c690",
+ "name": "aesop",
+ "inputRev?": "master"}},
+ {"git":
+ {"url": "https://github.com/leanprover/std4",
+ "subDir?": null,
+ "rev": "24897887905b3a1254b244369f5dd2cf6174b0ee",
+ "name": "std",
+ "inputRev?": "main"}}]}
diff --git a/tests/lean/misc-loops/lakefile.lean b/tests/lean/misc-loops/lakefile.lean
index 0d20ba1f..097c0a7d 100644
--- a/tests/lean/misc-loops/lakefile.lean
+++ b/tests/lean/misc-loops/lakefile.lean
@@ -4,15 +4,9 @@ open Lake DSL
require mathlib from git
"https://github.com/leanprover-community/mathlib4.git"
-package «loops» {
- -- add package configuration options here
-}
+package «loops» {}
-lean_lib «Base» {
- -- add library configuration options here
-}
-
-lean_lib «Loops» {
- -- add library configuration options here
-}
+lean_lib «Base» {}
+@[default_target]
+lean_lib «Loops» {}
diff --git a/tests/lean/misc-loops/lean-toolchain b/tests/lean/misc-loops/lean-toolchain
new file mode 100644
index 00000000..bbf57f10
--- /dev/null
+++ b/tests/lean/misc-loops/lean-toolchain
@@ -0,0 +1 @@
+leanprover/lean4:nightly-2023-01-21
diff --git a/tests/lean/misc-no_nested_borrows/NoNestedBorrows.lean b/tests/lean/misc-no_nested_borrows/NoNestedBorrows.lean
index a20ee9fd..cf7783b2 100644
--- a/tests/lean/misc-no_nested_borrows/NoNestedBorrows.lean
+++ b/tests/lean/misc-no_nested_borrows/NoNestedBorrows.lean
@@ -5,7 +5,9 @@ import Base.Primitives
structure OpaqueDefs where
/- [no_nested_borrows::Pair] -/
- structure pair_t (T1 T2 : Type) where pair_x : T1 pair_y : T2
+ structure pair_t (T1 T2 : Type) where
+ pair_x : T1
+ pair_y : T2
/- [no_nested_borrows::List] -/
inductive list_t (T : Type) :=
@@ -13,16 +15,20 @@ structure OpaqueDefs where
| ListNil : list_t T
/- [no_nested_borrows::One] -/
- inductive one_t (T1 : Type) := | OneOne : T1 -> one_t T1
+ inductive one_t (T1 : Type) :=
+ | OneOne : T1 -> one_t T1
/- [no_nested_borrows::EmptyEnum] -/
- inductive empty_enum_t := | EmptyEnumEmpty : empty_enum_t
+ inductive empty_enum_t :=
+ | EmptyEnumEmpty : empty_enum_t
/- [no_nested_borrows::Enum] -/
- inductive enum_t := | EnumVariant1 : enum_t | EnumVariant2 : enum_t
+ inductive enum_t :=
+ | EnumVariant1 : enum_t
+ | EnumVariant2 : enum_t
/- [no_nested_borrows::EmptyStruct] -/
- structure empty_struct_t where
+ structure empty_struct_t where
/- [no_nested_borrows::Sum] -/
inductive sum_t (T1 T2 : Type) :=
@@ -446,10 +452,8 @@ structure OpaqueDefs where
/- [no_nested_borrows::StructWithTuple] -/
structure struct_with_tuple_t (T1 T2 : Type) where
-
struct_with_tuple_p : (T1 × T2)
-
/- [no_nested_borrows::new_tuple1] -/
def new_tuple1_fwd : Result (struct_with_tuple_t UInt32 UInt32) :=
Result.ret
@@ -476,10 +480,8 @@ structure OpaqueDefs where
/- [no_nested_borrows::StructWithPair] -/
structure struct_with_pair_t (T1 T2 : Type) where
-
struct_with_pair_p : pair_t T1 T2
-
/- [no_nested_borrows::new_pair1] -/
def new_pair1_fwd : Result (struct_with_pair_t UInt32 UInt32) :=
Result.ret
diff --git a/tests/lean/misc-no_nested_borrows/lake-manifest.json b/tests/lean/misc-no_nested_borrows/lake-manifest.json
new file mode 100644
index 00000000..57b071ca
--- /dev/null
+++ b/tests/lean/misc-no_nested_borrows/lake-manifest.json
@@ -0,0 +1,27 @@
+{"version": 4,
+ "packagesDir": "./lake-packages",
+ "packages":
+ [{"git":
+ {"url": "https://github.com/leanprover-community/mathlib4.git",
+ "subDir?": null,
+ "rev": "4037792ead804d7bfa8868e2c4684d4223c15ece",
+ "name": "mathlib",
+ "inputRev?": null}},
+ {"git":
+ {"url": "https://github.com/gebner/quote4",
+ "subDir?": null,
+ "rev": "2412c4fdf4a8b689f4467618e5e7b371ae5014aa",
+ "name": "Qq",
+ "inputRev?": "master"}},
+ {"git":
+ {"url": "https://github.com/JLimperg/aesop",
+ "subDir?": null,
+ "rev": "7fe9ecd9339b0e1796e89d243b776849c305c690",
+ "name": "aesop",
+ "inputRev?": "master"}},
+ {"git":
+ {"url": "https://github.com/leanprover/std4",
+ "subDir?": null,
+ "rev": "24897887905b3a1254b244369f5dd2cf6174b0ee",
+ "name": "std",
+ "inputRev?": "main"}}]}
diff --git a/tests/lean/misc-no_nested_borrows/lakefile.lean b/tests/lean/misc-no_nested_borrows/lakefile.lean
index e4460813..58619110 100644
--- a/tests/lean/misc-no_nested_borrows/lakefile.lean
+++ b/tests/lean/misc-no_nested_borrows/lakefile.lean
@@ -4,15 +4,9 @@ open Lake DSL
require mathlib from git
"https://github.com/leanprover-community/mathlib4.git"
-package «no_nested_borrows» {
- -- add package configuration options here
-}
+package «no_nested_borrows» {}
-lean_lib «Base» {
- -- add library configuration options here
-}
-
-lean_lib «NoNestedBorrows» {
- -- add library configuration options here
-}
+lean_lib «Base» {}
+@[default_target]
+lean_lib «NoNestedBorrows» {}
diff --git a/tests/lean/misc-no_nested_borrows/lean-toolchain b/tests/lean/misc-no_nested_borrows/lean-toolchain
new file mode 100644
index 00000000..bbf57f10
--- /dev/null
+++ b/tests/lean/misc-no_nested_borrows/lean-toolchain
@@ -0,0 +1 @@
+leanprover/lean4:nightly-2023-01-21
diff --git a/tests/lean/misc-paper/lake-manifest.json b/tests/lean/misc-paper/lake-manifest.json
new file mode 100644
index 00000000..57b071ca
--- /dev/null
+++ b/tests/lean/misc-paper/lake-manifest.json
@@ -0,0 +1,27 @@
+{"version": 4,
+ "packagesDir": "./lake-packages",
+ "packages":
+ [{"git":
+ {"url": "https://github.com/leanprover-community/mathlib4.git",
+ "subDir?": null,
+ "rev": "4037792ead804d7bfa8868e2c4684d4223c15ece",
+ "name": "mathlib",
+ "inputRev?": null}},
+ {"git":
+ {"url": "https://github.com/gebner/quote4",
+ "subDir?": null,
+ "rev": "2412c4fdf4a8b689f4467618e5e7b371ae5014aa",
+ "name": "Qq",
+ "inputRev?": "master"}},
+ {"git":
+ {"url": "https://github.com/JLimperg/aesop",
+ "subDir?": null,
+ "rev": "7fe9ecd9339b0e1796e89d243b776849c305c690",
+ "name": "aesop",
+ "inputRev?": "master"}},
+ {"git":
+ {"url": "https://github.com/leanprover/std4",
+ "subDir?": null,
+ "rev": "24897887905b3a1254b244369f5dd2cf6174b0ee",
+ "name": "std",
+ "inputRev?": "main"}}]}
diff --git a/tests/lean/misc-paper/lakefile.lean b/tests/lean/misc-paper/lakefile.lean
index d8affff8..75d7208e 100644
--- a/tests/lean/misc-paper/lakefile.lean
+++ b/tests/lean/misc-paper/lakefile.lean
@@ -4,15 +4,9 @@ open Lake DSL
require mathlib from git
"https://github.com/leanprover-community/mathlib4.git"
-package «paper» {
- -- add package configuration options here
-}
+package «paper» {}
-lean_lib «Base» {
- -- add library configuration options here
-}
-
-lean_lib «Paper» {
- -- add library configuration options here
-}
+lean_lib «Base» {}
+@[default_target]
+lean_lib «Paper» {}
diff --git a/tests/lean/misc-paper/lean-toolchain b/tests/lean/misc-paper/lean-toolchain
new file mode 100644
index 00000000..bbf57f10
--- /dev/null
+++ b/tests/lean/misc-paper/lean-toolchain
@@ -0,0 +1 @@
+leanprover/lean4:nightly-2023-01-21
diff --git a/tests/lean/misc-polonius_list/lake-manifest.json b/tests/lean/misc-polonius_list/lake-manifest.json
new file mode 100644
index 00000000..57b071ca
--- /dev/null
+++ b/tests/lean/misc-polonius_list/lake-manifest.json
@@ -0,0 +1,27 @@
+{"version": 4,
+ "packagesDir": "./lake-packages",
+ "packages":
+ [{"git":
+ {"url": "https://github.com/leanprover-community/mathlib4.git",
+ "subDir?": null,
+ "rev": "4037792ead804d7bfa8868e2c4684d4223c15ece",
+ "name": "mathlib",
+ "inputRev?": null}},
+ {"git":
+ {"url": "https://github.com/gebner/quote4",
+ "subDir?": null,
+ "rev": "2412c4fdf4a8b689f4467618e5e7b371ae5014aa",
+ "name": "Qq",
+ "inputRev?": "master"}},
+ {"git":
+ {"url": "https://github.com/JLimperg/aesop",
+ "subDir?": null,
+ "rev": "7fe9ecd9339b0e1796e89d243b776849c305c690",
+ "name": "aesop",
+ "inputRev?": "master"}},
+ {"git":
+ {"url": "https://github.com/leanprover/std4",
+ "subDir?": null,
+ "rev": "24897887905b3a1254b244369f5dd2cf6174b0ee",
+ "name": "std",
+ "inputRev?": "main"}}]}
diff --git a/tests/lean/misc-polonius_list/lakefile.lean b/tests/lean/misc-polonius_list/lakefile.lean
index f941effc..e89d4259 100644
--- a/tests/lean/misc-polonius_list/lakefile.lean
+++ b/tests/lean/misc-polonius_list/lakefile.lean
@@ -4,15 +4,9 @@ open Lake DSL
require mathlib from git
"https://github.com/leanprover-community/mathlib4.git"
-package «polonius_list» {
- -- add package configuration options here
-}
+package «polonius_list» {}
-lean_lib «Base» {
- -- add library configuration options here
-}
-
-lean_lib «PoloniusList» {
- -- add library configuration options here
-}
+lean_lib «Base» {}
+@[default_target]
+lean_lib «PoloniusList» {}
diff --git a/tests/lean/misc-polonius_list/lean-toolchain b/tests/lean/misc-polonius_list/lean-toolchain
new file mode 100644
index 00000000..bbf57f10
--- /dev/null
+++ b/tests/lean/misc-polonius_list/lean-toolchain
@@ -0,0 +1 @@
+leanprover/lean4:nightly-2023-01-21