From a845071c6ab36da0cb8c82b17b461b4f2f0342f5 Mon Sep 17 00:00:00 2001 From: Chantal Keller Date: Tue, 28 Jan 2020 14:42:07 +0100 Subject: Best practice on axiom --- src/BEST_PRACTICE.md | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'src') diff --git a/src/BEST_PRACTICE.md b/src/BEST_PRACTICE.md index ba15070..d72c112 100644 --- a/src/BEST_PRACTICE.md +++ b/src/BEST_PRACTICE.md @@ -1,7 +1,8 @@ # Proofs ## Axioms -No axiom should be added. No library adding axioms should be imported. +No axiom should be added. No library adding axioms should be imported +(except Int63 and Array). # Code organization -- cgit From 7ad0aff65751133b298ef41861ed8cd688cf18eb Mon Sep 17 00:00:00 2001 From: Chantal Keller Date: Sat, 1 Feb 2020 14:52:31 +0100 Subject: Documentation --- src/BEST_PRACTICE.md | 3 +++ 1 file changed, 3 insertions(+) (limited to 'src') diff --git a/src/BEST_PRACTICE.md b/src/BEST_PRACTICE.md index d72c112..783ef82 100644 --- a/src/BEST_PRACTICE.md +++ b/src/BEST_PRACTICE.md @@ -6,6 +6,9 @@ No axiom should be added. No library adding axioms should be imported # Code organization +## Documentation +Every OCaml module comes with a documented interface. + ## Theories Theories are organized in sub-directories whose names are the names of -- cgit From 82fd19bc1c16782649c741548edb0649522ff900 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Tue, 25 Feb 2020 08:29:03 +0100 Subject: Do not call Coqlib resolution at linking time (#59) This was triggering an exception in async mode (and probably with static linking too), where ML code is loaded before `.vo` files. Fixes #58 --- src/lia/lia.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'src') diff --git a/src/lia/lia.ml b/src/lia/lia.ml index d546559..53ee55d 100644 --- a/src/lia/lia.ml +++ b/src/lia/lia.ml @@ -117,7 +117,7 @@ let smt_Atom_to_micromega_formula tbl ha = (* specialized fold *) -let default_constr = Structures.econstr_of_constr (mkInt 0) +let default_constr = lazy (Structures.econstr_of_constr (mkInt 0)) let default_tag = Structures.Micromega_plugin_Mutils.Tag.from 0 (* morphism for general formulas *) @@ -137,7 +137,7 @@ let rec smt_Form_to_coq_micromega_formula tbl l = match Form.pform l with | Fatom ha -> A (smt_Atom_to_micromega_formula tbl ha, - default_tag,default_constr) + default_tag, Lazy.force default_constr) | Fapp (Ftrue, _) -> TT | Fapp (Ffalse, _) -> FF | Fapp (Fand, l) -> binop_array smt_Form_to_coq_micromega_formula tbl (fun x y -> C (x,y)) TT l -- cgit From dfbf0a5674ae1ab0dc68c15ae4b5df8cc439b741 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Tue, 25 Feb 2020 08:30:04 +0100 Subject: Search correctly for `num` library (#60) We fix the way SMTCoq searches for the num library, both when building and when generating .merlin. --- src/versions/standard/Makefile.local | 4 ++++ 1 file changed, 4 insertions(+) (limited to 'src') diff --git a/src/versions/standard/Makefile.local b/src/versions/standard/Makefile.local index 045af88..a5fad33 100644 --- a/src/versions/standard/Makefile.local +++ b/src/versions/standard/Makefile.local @@ -22,6 +22,10 @@ clean:: CAMLLEX = $(CAMLBIN)ocamllex CAMLYACC = $(CAMLBIN)ocamlyacc +CAMLPKGS += -package num + +merlin-hook:: + $(HIDE)echo 'PKG num' >> .merlin %.ml : %.mll $(CAMLLEX) $< -- cgit From c296b2d06a70f1603916a2450ce49f6c98270a39 Mon Sep 17 00:00:00 2001 From: ckeller Date: Thu, 27 Feb 2020 09:28:50 +0100 Subject: Revert "Search correctly for `num` library (#60)" (#61) This reverts commit dfbf0a5674ae1ab0dc68c15ae4b5df8cc439b741. --- src/versions/standard/Makefile.local | 4 ---- 1 file changed, 4 deletions(-) (limited to 'src') diff --git a/src/versions/standard/Makefile.local b/src/versions/standard/Makefile.local index a5fad33..045af88 100644 --- a/src/versions/standard/Makefile.local +++ b/src/versions/standard/Makefile.local @@ -22,10 +22,6 @@ clean:: CAMLLEX = $(CAMLBIN)ocamllex CAMLYACC = $(CAMLBIN)ocamlyacc -CAMLPKGS += -package num - -merlin-hook:: - $(HIDE)echo 'PKG num' >> .merlin %.ml : %.mll $(CAMLLEX) $< -- cgit From eaa6a62db567c61c9a40af816a9e839eefaffa21 Mon Sep 17 00:00:00 2001 From: Chantal Keller Date: Fri, 28 Feb 2020 15:11:04 +0100 Subject: Remove useless code --- src/Conversion_tactics.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src') diff --git a/src/Conversion_tactics.v b/src/Conversion_tactics.v index ecf1be8..cb0c090 100644 --- a/src/Conversion_tactics.v +++ b/src/Conversion_tactics.v @@ -457,4 +457,4 @@ End nat_convert_type. Module nat_convert_mod := convert nat_convert_type. -Ltac nat_convert := fold Nat.add Nat.mul Nat.leb Nat.ltb Nat.eqb; nat_convert_mod.convert. +Ltac nat_convert := nat_convert_mod.convert. -- cgit From 31b398dc8bc7f6d62ea9e38504045aaa2c2fd018 Mon Sep 17 00:00:00 2001 From: Chantal Keller Date: Fri, 28 Feb 2020 16:36:06 +0100 Subject: Better error messages when veriT fails --- src/verit/verit.ml | 11 ++++++++--- 1 file changed, 8 insertions(+), 3 deletions(-) (limited to 'src') diff --git a/src/verit/verit.ml b/src/verit/verit.ml index 17a230f..c94f53c 100644 --- a/src/verit/verit.ml +++ b/src/verit/verit.ml @@ -185,20 +185,25 @@ let call_verit _ rt ro ra' rf' first lsmt = let win = open_in wname in - let raise_warnings () = + let raise_warnings_errors () = try while true do let l = input_line win in + let n = String.length l in if l = "warning : proof_done: status is still open" then raise Unknown + else if n >= 7 && String.sub l 0 7 = "warning" then + Structures.warning "verit-warning" ("veriT outputted the warning: " ^ (String.sub l 7 (n-7))) + else if n >= 8 && String.sub l 0 8 = "error : " then + Structures.error ("veriT failed with the error: " ^ (String.sub l 8 (n-8))) else - Structures.warning "verit-warning" ("Verit.call_verit: command " ^ command ^ " outputs the warning: " ^ l); + Structures.error ("veriT failed with the error: " ^ l) done with End_of_file -> () in try if exit_code <> 0 then Structures.warning "verit-non-zero-exit-code" ("Verit.call_verit: command " ^ command ^ " exited with code " ^ string_of_int exit_code); - raise_warnings (); + raise_warnings_errors (); let res = import_trace ra' rf' logfilename (Some first) lsmt in close_in win; Sys.remove wname; res with x -> close_in win; Sys.remove wname; -- cgit From baeb3e355eaa0e0dd0601c3a9265e996ea534512 Mon Sep 17 00:00:00 2001 From: Chantal Keller Date: Tue, 3 Mar 2020 10:16:28 +0100 Subject: veriT does not distinguish between warnings and errors (#64) --- src/verit/verit.ml | 2 ++ 1 file changed, 2 insertions(+) (limited to 'src') diff --git a/src/verit/verit.ml b/src/verit/verit.ml index c94f53c..39f60c0 100644 --- a/src/verit/verit.ml +++ b/src/verit/verit.ml @@ -192,6 +192,8 @@ let call_verit _ rt ro ra' rf' first lsmt = let n = String.length l in if l = "warning : proof_done: status is still open" then raise Unknown + else if l = "Invalid memory reference" then + Structures.warning "verit-warning" ("veriT outputted the warning: " ^ l) else if n >= 7 && String.sub l 0 7 = "warning" then Structures.warning "verit-warning" ("veriT outputted the warning: " ^ (String.sub l 7 (n-7))) else if n >= 8 && String.sub l 0 8 = "error : " then -- cgit From a3146935a48337634f6810d53a7cc7302cb61d47 Mon Sep 17 00:00:00 2001 From: Chantal Keller Date: Wed, 25 Mar 2020 18:46:08 +0100 Subject: make test does not need cleaning anymore --- src/versions/standard/Makefile.local | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'src') diff --git a/src/versions/standard/Makefile.local b/src/versions/standard/Makefile.local index 045af88..089ae9a 100644 --- a/src/versions/standard/Makefile.local +++ b/src/versions/standard/Makefile.local @@ -5,16 +5,16 @@ test : - cd ../unit-tests; make + cd ../unit-tests; make cleanvo; make ztest : - cd ../unit-tests; make zchaff + cd ../unit-tests; make cleanvo; make zchaff vtest : - cd ../unit-tests; make verit + cd ../unit-tests; make cleanvo; make verit lfsctest : - cd ../unit-tests; make lfsc + cd ../unit-tests; make cleanvo; make lfsc clean:: cd ../unit-tests; make clean -- cgit From 80a54a0e1974729d4756d2cc8483a2548c8dd2d0 Mon Sep 17 00:00:00 2001 From: ckeller Date: Thu, 26 Mar 2020 12:14:05 +0100 Subject: Test asynchronous and make the selected lemmas persistant (#66) * Add a test target for asynchronous proof checking (does not fully reflect the coqide behavior though) * Make the selected lemmas persistant Co-authored-by: Chantal Keller --- src/versions/standard/Makefile.local | 3 +++ src/versions/standard/g_smtcoq_standard.ml4 | 30 ++++++++++++++++++++++++----- 2 files changed, 28 insertions(+), 5 deletions(-) (limited to 'src') diff --git a/src/versions/standard/Makefile.local b/src/versions/standard/Makefile.local index 089ae9a..8abc72c 100644 --- a/src/versions/standard/Makefile.local +++ b/src/versions/standard/Makefile.local @@ -16,6 +16,9 @@ vtest : lfsctest : cd ../unit-tests; make cleanvo; make lfsc +paralleltest : + cd ../unit-tests; make parallel + clean:: cd ../unit-tests; make clean diff --git a/src/versions/standard/g_smtcoq_standard.ml4 b/src/versions/standard/g_smtcoq_standard.ml4 index bf923cc..6c3b8cf 100644 --- a/src/versions/standard/g_smtcoq_standard.ml4 +++ b/src/versions/standard/g_smtcoq_standard.ml4 @@ -80,17 +80,37 @@ TACTIC EXTEND Tactic_zchaff | [ "zchaff_bool_no_check" ] -> [ Zchaff.tactic_no_check () ] END -let lemmas_list = ref [] +let lemmas_list = Summary.ref ~name:"Selected lemmas" [] + +let cache_lemmas (_, lems) = + lemmas_list := lems + +let declare_lemmas : Structures.constr_expr list -> Libobject.obj = + let open Libobject in + declare_object + { + (default_object "LEMMAS") with + cache_function = cache_lemmas; + load_function = (fun _ -> cache_lemmas); + } + +let add_lemmas lems = + Lib.add_anonymous_leaf (declare_lemmas (lems @ !lemmas_list)) + +let clear_lemmas () = + Lib.add_anonymous_leaf (declare_lemmas []) + +let get_lemmas () = !lemmas_list VERNAC COMMAND EXTEND Add_lemma CLASSIFIED AS SIDEFF -| [ "Add_lemmas" constr_list(lems) ] -> [ lemmas_list := lems @ !lemmas_list ] -| [ "Clear_lemmas" ] -> [ lemmas_list := [] ] +| [ "Add_lemmas" constr_list(lems) ] -> [ add_lemmas lems ] +| [ "Clear_lemmas" ] -> [ clear_lemmas () ] END TACTIC EXTEND Tactic_verit -| [ "verit_bool_base" constr_list(lpl) ] -> [ Verit.tactic (List.map EConstr.Unsafe.to_constr lpl) !lemmas_list ] -| [ "verit_bool_no_check_base" constr_list(lpl) ] -> [ Verit.tactic_no_check (List.map EConstr.Unsafe.to_constr lpl) !lemmas_list ] +| [ "verit_bool_base" constr_list(lpl) ] -> [ Verit.tactic (List.map EConstr.Unsafe.to_constr lpl) (get_lemmas ()) ] +| [ "verit_bool_no_check_base" constr_list(lpl) ] -> [ Verit.tactic_no_check (List.map EConstr.Unsafe.to_constr lpl) (get_lemmas ()) ] END TACTIC EXTEND Tactic_cvc4 -- cgit