diff options
author | Jonathan Protzenko | 2023-02-02 23:36:14 -0800 |
---|---|---|
committer | Son HO | 2023-06-04 21:44:33 +0200 |
commit | 40e7df701d246faa453003374206014606ca6b6d (patch) | |
tree | 4f4a199c90ce53937eae8ec4ecb9e0d1f7564a2c | |
parent | dad646759a3ab9175c8797f144dec9d8e07b54b3 (diff) |
WIP
Diffstat (limited to '')
-rw-r--r-- | backends/lean/primitives.lean | 76 | ||||
-rw-r--r-- | compiler/Extract.ml | 10 | ||||
-rw-r--r-- | compiler/ExtractBase.ml | 4 | ||||
-rw-r--r-- | compiler/Translate.ml | 21 | ||||
-rw-r--r-- | tests/lean/hashmap_on_disk/Base/Primitives.lean | 76 | ||||
-rw-r--r-- | tests/lean/hashmap_on_disk/HashmapMain/Clauses/Template.lean | 113 | ||||
-rw-r--r-- | tests/lean/hashmap_on_disk/HashmapMain/Funs.lean | 8 | ||||
-rw-r--r-- | tests/lean/hashmap_on_disk/HashmapMain/Opaque.lean | 18 | ||||
-rw-r--r-- | tests/lean/hashmap_on_disk/HashmapMain/Types.lean | 4 | ||||
-rw-r--r-- | tests/lean/hashmap_on_disk/lake-manifest.json | 27 |
10 files changed, 286 insertions, 71 deletions
diff --git a/backends/lean/primitives.lean b/backends/lean/primitives.lean index 0a51aacd..79958d94 100644 --- a/backends/lean/primitives.lean +++ b/backends/lean/primitives.lean @@ -1,4 +1,5 @@ import Lean +import Lean.Meta.Tactic.Simp import Init.Data.List.Basic import Mathlib.Tactic.RunCmd @@ -75,7 +76,7 @@ macro "let" h:ident " : " e:term " <-- " f:term : doElem => -- Silly example of the kind of reasoning that this notation enables #eval do let h: y <-- .ret (0: Nat) - let _: y = 0 := by cases h; simp + let _: y = 0 := by cases h; decide let r: { x: Nat // x = 0 } := ⟨ y, by assumption ⟩ .ret r @@ -111,6 +112,23 @@ macro "let" h:ident " : " e:term " <-- " f:term : doElem => -- library_search." Try to settle this with a Lean expert on what is the most -- productive way to go about this? +-- One needs to perform a little bit of reasoning in order to successfully +-- inject constants into USize, so we provide a general-purpose macro + +syntax "intlit" : tactic + +macro_rules + | `(tactic| intlit) => `(tactic| + match USize.size, usize_size_eq with + | _, Or.inl rfl => decide + | _, Or.inr rfl => decide) + +-- This is how the macro is expected to be used +#eval USize.ofNatCore 0 (by intlit) + +-- Also works for other integer types (at the expense of a needless disjunction) +#eval UInt32.ofNatCore 0 (by intlit) + -- Further thoughts: look at what has been done here: -- https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Data/Fin/Basic.lean -- and @@ -133,7 +151,12 @@ def USize.checked_sub (n: USize) (m: USize): result USize := fail integerOverflow def USize.checked_add (n: USize) (m: USize): result USize := - if h: n.val + m.val < USize.size then + if h: n.val.val + m.val.val <= 4294967295 then + .ret ⟨ n.val.val + m.val.val, by + have h': 4294967295 < USize.size := by intlit + apply Nat.lt_of_le_of_lt h h' + ⟩ + else if h: n.val + m.val < USize.size then .ret ⟨ n.val + m.val, h ⟩ else .fail integerOverflow @@ -149,7 +172,12 @@ def USize.checked_rem (n: USize) (m: USize): result USize := .fail integerOverflow def USize.checked_mul (n: USize) (m: USize): result USize := - if h: n.val * m.val < USize.size then + if h: n.val.val * m.val.val <= 4294967295 then + .ret ⟨ n.val.val * m.val.val, by + have h': 4294967295 < USize.size := by intlit + apply Nat.lt_of_le_of_lt h h' + ⟩ + else if h: n.val * m.val < USize.size then .ret ⟨ n.val * m.val, h ⟩ else .fail integerOverflow @@ -187,22 +215,6 @@ def scalar_cast { src: Type } (dst: Type) [ MachineInteger src ] [ MachineIntege else .fail integerOverflow --- One needs to perform a little bit of reasoning in order to successfully --- inject constants into USize, so we provide a general-purpose macro - -syntax "intlit" : tactic - -macro_rules - | `(tactic| intlit) => `(tactic| - match USize.size, usize_size_eq with - | _, Or.inl rfl => decide - | _, Or.inr rfl => decide) - --- This is how the macro is expected to be used -#eval USize.ofNatCore 0 (by intlit) - --- Also works for other integer types (at the expense of a needless disjunction) -#eval UInt32.ofNatCore 0 (by intlit) -- Test behavior... #eval assert! USize.checked_sub 10 20 == fail integerOverflow; 0 @@ -267,7 +279,14 @@ def vec_push_back_old (α : Type u) (v : vec α) (x : α) : { res: result (vec def vec_push_back (α : Type u) (v : vec α) (x : α) : result (vec α) := - if h : List.length v.val + 1 < USize.size then + if h : List.length v.val + 1 <= 4294967295 then + return ⟨ List.concat v.val x, + by + rw [List.length_concat] + have h': 4294967295 < USize.size := by intlit + apply Nat.lt_of_le_of_lt h h' + ⟩ + else if h: List.length v.val + 1 < USize.size then return ⟨List.concat v.val x, by rw [List.length_concat] @@ -340,10 +359,15 @@ syntax (name := assert) "#assert" term: command @[command_elab assert] def assertImpl : CommandElab := fun (_stx: Syntax) => do - logInfo "Hello World" - -def ignore (a: Prop) (_x: a) := () - -#eval ignore (2 == 2) (by simp) - + logInfo "Reducing and asserting: " + logInfo _stx[1] + runTermElabM (fun _ => do + let e ← Term.elabTerm _stx[1] none + logInfo (Expr.dbgToString e) + -- How to evaluate the term and compare the result to true? + pure ()) + -- logInfo (Expr.dbgToString (``true)) + -- throwError "TODO: assert" + +#eval 2 == 2 #assert (2 == 2) diff --git a/compiler/Extract.ml b/compiler/Extract.ml index d707dc81..e1b2b23f 100644 --- a/compiler/Extract.ml +++ b/compiler/Extract.ml @@ -476,8 +476,10 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string) in let fun_name (fname : fun_name) (num_loops : int) (loop_id : LoopId.id option) (num_rgs : int) (rg : region_group_info option) (filter_info : bool * int) + (missing_body: bool) : string = let fname = fun_name_to_snake_case fname in + let fname = if !backend = Lean && missing_body then "opaque_defs." ^ fname else fname in (* Compute the suffix *) let suffix = default_fun_suffix num_loops loop_id num_rgs rg filter_info in (* Concatenate *) @@ -1371,7 +1373,6 @@ let extract_fun_decl_register_names (ctx : extraction_ctx) (keep_fwd : bool) ctx in let ctx = List.fold_left register_decreases ctx (fwd :: loop_fwds) in - (* Register the function names *) let register_fun ctx f = ctx_add_fun_decl (keep_fwd, def) f ctx in let register_funs ctx fl = List.fold_left register_fun ctx fl in (* Register the forward functions' names *) @@ -2227,7 +2228,12 @@ let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter) let use_forall = is_opaque_coq && def.signature.type_params <> [] in (* *) let qualif = ctx.fmt.fun_decl_kind_to_qualif kind in - F.pp_print_string fmt (qualif ^ " " ^ def_name); + (* For Lean: we generate a record of assumed functions *) + if not (!backend = Lean && (kind = Assumed || kind = Declared)) then begin + F.pp_print_string fmt qualif; + F.pp_print_space fmt () + end; + F.pp_print_string fmt def_name; F.pp_print_space fmt (); if use_forall then ( F.pp_print_string fmt ":"; diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml index 77170b5b..98a29daf 100644 --- a/compiler/ExtractBase.ml +++ b/compiler/ExtractBase.ml @@ -168,6 +168,7 @@ type formatter = { int -> region_group_info option -> bool * int -> + bool -> string; (** Compute the name of a regular (non-assumed) function. @@ -187,6 +188,7 @@ type formatter = { The number of extracted backward functions if not necessarily equal to the number of region groups, because we may have filtered some of them. + - whether there is a body or not (indicates assumed function) TODO: use the fun id for the assumed functions. *) decreases_clause_name : @@ -774,7 +776,7 @@ let ctx_add_fun_decl (trans_group : bool * pure_fun_translation) in let name = ctx.fmt.fun_name def.basename def.num_loops def.loop_id num_rgs rg_info - (keep_fwd, num_backs) + (keep_fwd, num_backs) (def.body = None) in ctx_add (FunId (FromLlbc (A.Regular def_id, def.loop_id, def.back_id))) diff --git a/compiler/Translate.ml b/compiler/Translate.ml index 0a1c8f9a..df7a750d 100644 --- a/compiler/Translate.ml +++ b/compiler/Translate.ml @@ -661,13 +661,24 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config) *) if config.extract_state_type && config.extract_fun_decls then export_state_type (); + if config.extract_opaque && config.extract_fun_decls && !Config.backend = Lean then begin + 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 + end; List.iter export_decl_group ctx.crate.declarations; + if config.extract_opaque && !Config.backend = Lean then begin + Format.pp_close_box fmt () + end; if config.extract_state_type && not config.extract_fun_decls then export_state_type () let extract_file (config : gen_config) (ctx : gen_ctx) (filename : string) (rust_module_name : string) (module_name : string) (custom_msg : string) - (custom_imports : string list) (custom_includes : string list) : unit = + ?(custom_variables: string list = []) + (custom_imports : string list) (custom_includes : string list) + : unit = (* Open the file and create the formatter *) let out = open_out filename in let fmt = Format.formatter_of_out_channel out in @@ -720,7 +731,11 @@ let extract_file (config : gen_config) (ctx : gen_ctx) (filename : string) (* Add the custom imports *) List.iter (fun m -> Printf.fprintf out "import %s\n" m) custom_imports; (* Add the custom includes *) - List.iter (fun m -> Printf.fprintf out "import %s\n" m) custom_includes + List.iter (fun m -> Printf.fprintf out "import %s\n" m) custom_includes; + if custom_variables <> [] then begin + Printf.fprintf out "\n"; + List.iter (fun m -> Printf.fprintf out "%s\n" m) custom_variables + end ); (* From now onwards, we use the formatter *) (* Set the margin *) @@ -1016,8 +1031,10 @@ let translate_module (filename : string) (dest_dir : string) (crate : A.crate) : [ module_name ^ module_delimiter ^ "Clauses" ^ module_delimiter ^ "Template"] else [] in + let custom_variables = if has_opaque_funs then [ "section variable (opaque_defs: OpaqueDefs)" ] else [] in extract_file fun_config gen_ctx fun_filename crate.A.name fun_module ": function definitions" [] + ~custom_variables ([ types_module ] @ opaque_funs_module @ clauses_module)) else let gen_config = diff --git a/tests/lean/hashmap_on_disk/Base/Primitives.lean b/tests/lean/hashmap_on_disk/Base/Primitives.lean index 0a51aacd..79958d94 100644 --- a/tests/lean/hashmap_on_disk/Base/Primitives.lean +++ b/tests/lean/hashmap_on_disk/Base/Primitives.lean @@ -1,4 +1,5 @@ import Lean +import Lean.Meta.Tactic.Simp import Init.Data.List.Basic import Mathlib.Tactic.RunCmd @@ -75,7 +76,7 @@ macro "let" h:ident " : " e:term " <-- " f:term : doElem => -- Silly example of the kind of reasoning that this notation enables #eval do let h: y <-- .ret (0: Nat) - let _: y = 0 := by cases h; simp + let _: y = 0 := by cases h; decide let r: { x: Nat // x = 0 } := ⟨ y, by assumption ⟩ .ret r @@ -111,6 +112,23 @@ macro "let" h:ident " : " e:term " <-- " f:term : doElem => -- library_search." Try to settle this with a Lean expert on what is the most -- productive way to go about this? +-- One needs to perform a little bit of reasoning in order to successfully +-- inject constants into USize, so we provide a general-purpose macro + +syntax "intlit" : tactic + +macro_rules + | `(tactic| intlit) => `(tactic| + match USize.size, usize_size_eq with + | _, Or.inl rfl => decide + | _, Or.inr rfl => decide) + +-- This is how the macro is expected to be used +#eval USize.ofNatCore 0 (by intlit) + +-- Also works for other integer types (at the expense of a needless disjunction) +#eval UInt32.ofNatCore 0 (by intlit) + -- Further thoughts: look at what has been done here: -- https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Data/Fin/Basic.lean -- and @@ -133,7 +151,12 @@ def USize.checked_sub (n: USize) (m: USize): result USize := fail integerOverflow def USize.checked_add (n: USize) (m: USize): result USize := - if h: n.val + m.val < USize.size then + if h: n.val.val + m.val.val <= 4294967295 then + .ret ⟨ n.val.val + m.val.val, by + have h': 4294967295 < USize.size := by intlit + apply Nat.lt_of_le_of_lt h h' + ⟩ + else if h: n.val + m.val < USize.size then .ret ⟨ n.val + m.val, h ⟩ else .fail integerOverflow @@ -149,7 +172,12 @@ def USize.checked_rem (n: USize) (m: USize): result USize := .fail integerOverflow def USize.checked_mul (n: USize) (m: USize): result USize := - if h: n.val * m.val < USize.size then + if h: n.val.val * m.val.val <= 4294967295 then + .ret ⟨ n.val.val * m.val.val, by + have h': 4294967295 < USize.size := by intlit + apply Nat.lt_of_le_of_lt h h' + ⟩ + else if h: n.val * m.val < USize.size then .ret ⟨ n.val * m.val, h ⟩ else .fail integerOverflow @@ -187,22 +215,6 @@ def scalar_cast { src: Type } (dst: Type) [ MachineInteger src ] [ MachineIntege else .fail integerOverflow --- One needs to perform a little bit of reasoning in order to successfully --- inject constants into USize, so we provide a general-purpose macro - -syntax "intlit" : tactic - -macro_rules - | `(tactic| intlit) => `(tactic| - match USize.size, usize_size_eq with - | _, Or.inl rfl => decide - | _, Or.inr rfl => decide) - --- This is how the macro is expected to be used -#eval USize.ofNatCore 0 (by intlit) - --- Also works for other integer types (at the expense of a needless disjunction) -#eval UInt32.ofNatCore 0 (by intlit) -- Test behavior... #eval assert! USize.checked_sub 10 20 == fail integerOverflow; 0 @@ -267,7 +279,14 @@ def vec_push_back_old (α : Type u) (v : vec α) (x : α) : { res: result (vec def vec_push_back (α : Type u) (v : vec α) (x : α) : result (vec α) := - if h : List.length v.val + 1 < USize.size then + if h : List.length v.val + 1 <= 4294967295 then + return ⟨ List.concat v.val x, + by + rw [List.length_concat] + have h': 4294967295 < USize.size := by intlit + apply Nat.lt_of_le_of_lt h h' + ⟩ + else if h: List.length v.val + 1 < USize.size then return ⟨List.concat v.val x, by rw [List.length_concat] @@ -340,10 +359,15 @@ syntax (name := assert) "#assert" term: command @[command_elab assert] def assertImpl : CommandElab := fun (_stx: Syntax) => do - logInfo "Hello World" - -def ignore (a: Prop) (_x: a) := () - -#eval ignore (2 == 2) (by simp) - + logInfo "Reducing and asserting: " + logInfo _stx[1] + runTermElabM (fun _ => do + let e ← Term.elabTerm _stx[1] none + logInfo (Expr.dbgToString e) + -- How to evaluate the term and compare the result to true? + pure ()) + -- logInfo (Expr.dbgToString (``true)) + -- throwError "TODO: assert" + +#eval 2 == 2 #assert (2 == 2) diff --git a/tests/lean/hashmap_on_disk/HashmapMain/Clauses/Template.lean b/tests/lean/hashmap_on_disk/HashmapMain/Clauses/Template.lean new file mode 100644 index 00000000..bf331d6e --- /dev/null +++ b/tests/lean/hashmap_on_disk/HashmapMain/Clauses/Template.lean @@ -0,0 +1,113 @@ +-- 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, n) + +syntax "hashmap_hash_map_allocate_slots_loop_decreases" term+ : tactic + +macro_rules +| `(tactic| hashmap_hash_map_allocate_slots_loop_decreases $slots $n) => + `(tactic| sorry) + +/- [hashmap_main::hashmap::HashMap::{0}::clear_slots]: termination measure -/ +@[simp] +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_slots_loop_decreases" term+ : tactic + +macro_rules +| `(tactic| hashmap_hash_map_clear_slots_loop_decreases $slots $i) => + `(tactic| sorry) + +/- [hashmap_main::hashmap::HashMap::{0}::insert_in_list]: termination measure -/ +@[simp] +def hashmap_hash_map_insert_in_list_loop_terminates (T : Type) (key : USize) + (value : T) (ls : hashmap_list_t T) := + (key, value, ls) + +syntax "hashmap_hash_map_insert_in_list_loop_decreases" term+ : tactic + +macro_rules +| `(tactic| hashmap_hash_map_insert_in_list_loop_decreases $key $value $ls) => + `(tactic| sorry) + +/- [hashmap_main::hashmap::HashMap::{0}::move_elements_from_list]: termination measure -/ +@[simp] +def hashmap_hash_map_move_elements_from_list_loop_terminates (T : Type) + (ntable : hashmap_hash_map_t T) (ls : hashmap_list_t T) := + (ntable, ls) + +syntax "hashmap_hash_map_move_elements_from_list_loop_decreases" term+ : tactic + +macro_rules +| `(tactic| hashmap_hash_map_move_elements_from_list_loop_decreases $ntable +$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, slots, i) + +syntax "hashmap_hash_map_move_elements_loop_decreases" term+ : tactic + +macro_rules +| `(tactic| hashmap_hash_map_move_elements_loop_decreases $ntable $slots $i) => + `(tactic| sorry) + +/- [hashmap_main::hashmap::HashMap::{0}::contains_key_in_list]: termination measure -/ +@[simp] +def hashmap_hash_map_contains_key_in_list_loop_terminates (T : Type) + (key : USize) (ls : hashmap_list_t T) := + (key, ls) + +syntax "hashmap_hash_map_contains_key_in_list_loop_decreases" term+ : tactic + +macro_rules +| `(tactic| hashmap_hash_map_contains_key_in_list_loop_decreases $key $ls) => + `(tactic| sorry) + +/- [hashmap_main::hashmap::HashMap::{0}::get_in_list]: termination measure -/ +@[simp] +def hashmap_hash_map_get_in_list_loop_terminates (T : Type) (key : USize) + (ls : hashmap_list_t T) := + (key, ls) + +syntax "hashmap_hash_map_get_in_list_loop_decreases" term+ : tactic + +macro_rules +| `(tactic| hashmap_hash_map_get_in_list_loop_decreases $key $ls) =>`(tactic| sorry) + +/- [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list]: termination measure -/ +@[simp] +def hashmap_hash_map_get_mut_in_list_loop_terminates (T : Type) + (ls : hashmap_list_t T) (key : USize) := + (ls, key) + +syntax "hashmap_hash_map_get_mut_in_list_loop_decreases" term+ : tactic + +macro_rules +| `(tactic| hashmap_hash_map_get_mut_in_list_loop_decreases $ls $key) => + `(tactic| sorry) + +/- [hashmap_main::hashmap::HashMap::{0}::remove_from_list]: termination measure -/ +@[simp] +def hashmap_hash_map_remove_from_list_loop_terminates (T : Type) (key : USize) + (ls : hashmap_list_t T) := + (key, ls) + +syntax "hashmap_hash_map_remove_from_list_loop_decreases" term+ : tactic + +macro_rules +| `(tactic| hashmap_hash_map_remove_from_list_loop_decreases $key $ls) => + `(tactic| sorry) + diff --git a/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean b/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean index 5e78d9cf..ffe3416a 100644 --- a/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean +++ b/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean @@ -5,6 +5,8 @@ import HashmapMain.Types import HashmapMain.Opaque import HashmapMain.Clauses.Template +section variable (opaque_defs: OpaqueDecls) + /- [hashmap_main::hashmap::hash_key] -/ def hashmap_hash_key_fwd (k : USize) : result USize := result.ret k @@ -637,15 +639,15 @@ def hashmap_test1_fwd : result Unit := /- Unit test for [hashmap_main::hashmap::test1] -/ -#assert (hashmap_test1_fwd = ret ()) +#assert (hashmap_test1_fwd = .ret ()) /- [hashmap_main::insert_on_disk] -/ def insert_on_disk_fwd (key : USize) (value : UInt64) (st : state) : result (state × Unit) := do - let (st0, hm) <- hashmap_utils_deserialize_fwd st + let (st0, hm) <- opaque_defs.hashmap_utils_deserialize_fwd st let hm0 <- hashmap_hash_map_insert_fwd_back UInt64 hm key value - let (st1, _) <- hashmap_utils_serialize_fwd hm0 st0 + let (st1, _) <- opaque_defs.hashmap_utils_serialize_fwd hm0 st0 result.ret (st1, ()) /- [hashmap_main::main] -/ diff --git a/tests/lean/hashmap_on_disk/HashmapMain/Opaque.lean b/tests/lean/hashmap_on_disk/HashmapMain/Opaque.lean index 87b10c59..8b41934d 100644 --- a/tests/lean/hashmap_on_disk/HashmapMain/Opaque.lean +++ b/tests/lean/hashmap_on_disk/HashmapMain/Opaque.lean @@ -3,11 +3,13 @@ import Base.Primitives import HashmapMain.Types -/- [hashmap_main::hashmap_utils::deserialize] -/ -axiom hashmap_utils_deserialize_fwd - : state -> result (state × (hashmap_hash_map_t UInt64)) - -/- [hashmap_main::hashmap_utils::serialize] -/ -axiom hashmap_utils_serialize_fwd - : hashmap_hash_map_t UInt64 -> state -> result (state × Unit) - +structure OpaqueDecls where + + /- [hashmap_main::hashmap_utils::deserialize] -/ + hashmap_utils_deserialize_fwd + : state -> result (state × (hashmap_hash_map_t UInt64)) + + /- [hashmap_main::hashmap_utils::serialize] -/ + hashmap_utils_serialize_fwd + : hashmap_hash_map_t UInt64 -> state -> result (state × Unit) + diff --git a/tests/lean/hashmap_on_disk/HashmapMain/Types.lean b/tests/lean/hashmap_on_disk/HashmapMain/Types.lean index d1cd9579..2a3ea462 100644 --- a/tests/lean/hashmap_on_disk/HashmapMain/Types.lean +++ b/tests/lean/hashmap_on_disk/HashmapMain/Types.lean @@ -15,7 +15,5 @@ structure hashmap_hash_map_t (T : Type) where 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 new file mode 100644 index 00000000..8ac53836 --- /dev/null +++ b/tests/lean/hashmap_on_disk/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": "583f6cfa4bced545c797216b32600d6211b753f9", + "name": "mathlib", + "inputRev?": null}}, + {"git": + {"url": "https://github.com/gebner/quote4", + "subDir?": null, + "rev": "7ac99aa3fac487bec1d5860e751b99c7418298cf", + "name": "Qq", + "inputRev?": "master"}}, + {"git": + {"url": "https://github.com/JLimperg/aesop", + "subDir?": null, + "rev": "ccff5d4ae7411c5fe741f3139950e8bddf353dea", + "name": "aesop", + "inputRev?": "master"}}, + {"git": + {"url": "https://github.com/leanprover/std4", + "subDir?": null, + "rev": "cda27d551340756d5ed6f9b83716a9db799c5537", + "name": "std", + "inputRev?": "main"}}]} |