Skip to content

Commit

Permalink
Fix mutable skipping in recursive mode
Browse files Browse the repository at this point in the history
I guess I never actually tested it? Not sure how it would ever have worked.

Fix #14
  • Loading branch information
SkySkimmer committed Nov 4, 2023
1 parent ee175a9 commit aaf62a8
Show file tree
Hide file tree
Showing 3 changed files with 14 additions and 1 deletion.
3 changes: 2 additions & 1 deletion src/tac2compile.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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 ->
Expand Down
1 change: 1 addition & 0 deletions tests/_CoqProject
Original file line number Diff line number Diff line change
Expand Up @@ -8,3 +8,4 @@ bug_10107.v
minibench.v
compiler_bug_4.v
compiler_bug_6.v
compiler_bug_14.v
11 changes: 11 additions & 0 deletions tests/compiler_bug_14.v
Original file line number Diff line number Diff line change
@@ -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
*)

0 comments on commit aaf62a8

Please sign in to comment.