diff options
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 |