From ee175a92cef0b12345391c96eac14e26437db695 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Sat, 4 Nov 2023 13:17:09 +0100 Subject: [PATCH 1/2] Add debug print of constants found by get_recursive_kns --- src/tac2compile.ml | 1 + 1 file changed, 1 insertion(+) diff --git a/src/tac2compile.ml b/src/tac2compile.ml index 341e9ee..f680cac 100644 --- a/src/tac2compile.ml +++ b/src/tac2compile.ml @@ -1121,6 +1121,7 @@ let compile ~recursive knl = if recursive then get_recursive_kns knl else knl in + debug Pp.(fun () -> str "Compiling constants " ++ prlist_with_sep spc (Tac2print.pr_tacref Id.Set.empty) knl); let file, ch, prefix = get_ml_filename () in let kns, exts, pp = pp_code recursive prefix knl in let fch = Format.formatter_of_out_channel ch in From aaf62a8386707f11943ff73952991e0cc5208607 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Sat, 4 Nov 2023 13:22:00 +0100 Subject: [PATCH 2/2] Fix mutable skipping in recursive mode I guess I never actually tested it? Not sure how it would ever have worked. Fix #14 --- src/tac2compile.ml | 3 ++- tests/_CoqProject | 1 + tests/compiler_bug_14.v | 11 +++++++++++ 3 files changed, 14 insertions(+), 1 deletion(-) create mode 100644 tests/compiler_bug_14.v diff --git a/src/tac2compile.ml b/src/tac2compile.ml index f680cac..0321695 100644 --- a/src/tac2compile.ml +++ b/src/tac2compile.ml @@ -1004,7 +1004,8 @@ let rec get_dependencies ((visited, skipped_mut, knl) as acc) kn = kndeps (KNset.add kn visited, skipped_mut, knl) in - (visited, skipped_mut, kn :: knl) + let knl = if data.gdata_mutable then knl else kn :: knl in + (visited, skipped_mut, knl) let warn_skipped_mut = CWarnings.create ~name:"tac2compile-skipped-mutable" ~category:CWarnings.CoreCategories.ltac2 (fun skipped_mut -> diff --git a/tests/_CoqProject b/tests/_CoqProject index 0fca7c6..c0c2606 100644 --- a/tests/_CoqProject +++ b/tests/_CoqProject @@ -8,3 +8,4 @@ bug_10107.v minibench.v compiler_bug_4.v compiler_bug_6.v +compiler_bug_14.v diff --git a/tests/compiler_bug_14.v b/tests/compiler_bug_14.v new file mode 100644 index 0000000..edfe167 --- /dev/null +++ b/tests/compiler_bug_14.v @@ -0,0 +1,11 @@ +From Ltac2 Require Import Ltac2. +Ltac2 mutable mut : unit := (). +Ltac2 test () := match mut with () => () end. + +From Ltac2Compiler Require Import Ltac2Compiler. + +Ltac2 Compile test. +(* +Dynlink error: execution of module initializers in the shared library failed: +File "plugins/ltac2/tac2env.ml", line 79, characters 2-8: Assertion failed +*)