Closed MSoegtropIMC closed 1 year ago
Where in the rewriter is it failing? (Can you also get a stack trace?) Some of the reification has been rewritten for performance for 0.0.7 (https://github.com/mit-plv/rewriter/pull/77) (see also the release notes of the tag), but if the rewriter is stack overflowing this makes me very pessimistic about Fiat Crypto, since AFAIK there's nothing particularly stack intensive in the rewriter.
I see what I can do about the stack trace, but it might be largish (with a stack limit of 64 MB).
fiat-crypto currently hangs on coq-coqprime. There is already a new version, but the opam package isn't through as yet.
Hmm - interesting. It dies on a Search
command, but only if Rewriter.Util.plugins.RewriterBuild
is imported. A minimal reproduction example is:
Require Import Rewriter.Util.plugins.RewriterBuild.
Print nat.
Search (?x + 0 = ?x).
Print nat.
which results in:
coq-rewriter.0.0.7 % coqc -I src/Rewriter/Util/plugins -R src/Rewriter Rewriter src/Rewriter/Demo_2.v
Inductive nat : Set := O : nat | S : nat -> nat.
Arguments S _%nat_scope
File "./src/Rewriter/Demo_2.v", line 3, characters 0-21:
Error: Stack overflow.
I added the two Print nat
commands to be sure.
I try to get it further down.
It is difficult to get a stack trace (lldbs
bt` command apparently does not work after a stack overflow (hangs)). I tried to sample the process once per ms and in there I get sometimes rather deep stack traces around some directory traversal.
How it comes that I can compile almost all of Coq Platform and then it dies here I really can't tell.
I got it down to this snipet:
Require Import Rewriter.Language.IdentifiersLibrary.
Print nat.
Search (?x + 0 = ?x).
Print nat.
Replacing the require with all requires and imports in this file (including Import EqNotations
) does not lead to a stack overflow.
Ah, and yes: when I comment out the "Search" command the file compiles fine.
It is difficult to get a stack trace (lldbs bt` command apparently does not work after a stack overflow (hangs)).
What about putting Set Debug "backtrace".
before the failing command?
I get sometimes rather deep stack traces around some directory traversal.
Can you be more specific?
Is the pattern searched important? (So as to have a hint about whether it is about the pattern-matching algorithm or about the browsing of the environment.)
@SkySkimmer:
With "Set Debug "backtrace" I get for the first 100 levels:
coq-rewriter.0.0.7 % coqc -q -w +implicit-core-hint-db,+implicits-in-term,+non-reversible-notation,+deprecated-intros-until-0,+deprecated-focus,+unused-intro-pattern,+deprecated-hint-constr,+fragile-hint-constr,+variable-collision,+unexpected-implicit-declaration,+omega-is-deprecated,+deprecated-instantiate-syntax,+non-recursive,+deprecated-hint-rewrite-without-locality,+deprecated-hint-without-locality,+deprecated-instance-without-locality,+undeclared-scope,+deprecated-typeclasses-transparency-without-locality,+future-coercion-class-field,unsupported-attributes -w -notation-overridden,-unusable-identifier -w -notation-overridden -w -notation-overridden -w -deprecated-native-compiler-option -native-compiler ondemand -I src/Rewriter/Util/plugins -R src/Rewriter Rewriter src/Rewriter/Demo2.v
While loading initial state:
Warning: Native compiler is disabled, -native-compiler ondemand option
ignored. [native-compiler-disabled,native-compiler]
Inductive nat : Set := O : nat | S : nat -> nat.
Arguments S _%nat_scope
File "./src/Rewriter/Demo2.v", line 4, characters 0-21:
Error:
Stack overflow.
Raised by primitive operation at Constr_matching.sub_match.try_aux.try_sub_match_rec.next in file "pretyping/constr_matching.ml", line 643, characters 22-54
Called from Constr_matching.sub_match.try_aux.try_sub_match_rec.next in file "pretyping/constr_matching.ml", line 643, characters 22-54
Called from Constr_matching.sub_match.try_aux.try_sub_match_rec.next in file "pretyping/constr_matching.ml", line 643, characters 22-54
Called from Constr_matching.sub_match.try_aux.try_sub_match_rec.next in file "pretyping/constr_matching.ml", line 643, characters 22-54
Called from Constr_matching.sub_match.try_aux.try_sub_match_rec.next in file "pretyping/constr_matching.ml", line 643, characters 22-54
Called from Constr_matching.sub_match.aux.next in file "pretyping/constr_matching.ml", line 543, characters 11-1023
Called from Constr_matching.sub_match.try_aux.try_sub_match_rec.next in file "pretyping/constr_matching.ml", line 643, characters 22-54
Called from Constr_matching.sub_match.try_aux.try_sub_match_rec.next in file "pretyping/constr_matching.ml", line 643, characters 22-54
Called from Constr_matching.sub_match.aux.next in file "pretyping/constr_matching.ml", line 543, characters 11-1023
Called from Constr_matching.sub_match.try_aux.try_sub_match_rec.next in file "pretyping/constr_matching.ml", line 643, characters 22-54
Called from Constr_matching.sub_match.aux.next in file "pretyping/constr_matching.ml", line 543, characters 11-1023
Called from Constr_matching.sub_match.try_aux in file "pretyping/constr_matching.ml", line 646, characters 4-27
Called from Constr_matching.sub_match.aux.next in file "pretyping/constr_matching.ml", line 543, characters 11-1023
Called from Constr_matching.sub_match.try_aux in file "pretyping/constr_matching.ml", line 646, characters 4-27
Called from Constr_matching.sub_match.aux.next in file "pretyping/constr_matching.ml", line 543, characters 11-1023
Called from Constr_matching.sub_match.try_aux.try_sub_match_rec.next in file "pretyping/constr_matching.ml", line 643, characters 22-54
Called from Constr_matching.sub_match.aux.next in file "pretyping/constr_matching.ml", line 543, characters 11-1023
Called from Constr_matching.sub_match.try_aux in file "pretyping/constr_matching.ml", line 646, characters 4-27
Called from Constr_matching.sub_match.aux.next in file "pretyping/constr_matching.ml", line 543, characters 11-1023
Called from Constr_matching.sub_match.try_aux.try_sub_match_rec.next in file "pretyping/constr_matching.ml", line 643, characters 22-54
Called from Constr_matching.sub_match.aux.next in file "pretyping/constr_matching.ml", line 543, characters 11-1023
Called from Constr_matching.sub_match.try_aux in file "pretyping/constr_matching.ml", line 646, characters 4-27
Called from Constr_matching.sub_match.aux.next in file "pretyping/constr_matching.ml", line 543, characters 11-1023
Called from Constr_matching.sub_match.try_aux.try_sub_match_rec.next in file "pretyping/constr_matching.ml", line 643, characters 22-54
Called from Constr_matching.sub_match.try_aux.try_sub_match_rec.next in file "pretyping/constr_matching.ml", line 643, characters 22-54
Called from Constr_matching.sub_match.aux.next in file "pretyping/constr_matching.ml", line 543, characters 11-1023
Called from Constr_matching.sub_match.try_aux.try_sub_match_rec.next in file "pretyping/constr_matching.ml", line 643, characters 22-54
Called from Constr_matching.sub_match.try_aux.try_sub_match_rec.next in file "pretyping/constr_matching.ml", line 643, characters 22-54
Called from Constr_matching.sub_match.aux.next in file "pretyping/constr_matching.ml", line 543, characters 11-1023
Called from Constr_matching.sub_match.try_aux.try_sub_match_rec.next in file "pretyping/constr_matching.ml", line 643, characters 22-54
Called from Constr_matching.sub_match.aux.next in file "pretyping/constr_matching.ml", line 543, characters 11-1023
Called from Constr_matching.sub_match.try_aux in file "pretyping/constr_matching.ml", line 646, characters 4-27
Called from Constr_matching.sub_match.aux.next in file "pretyping/constr_matching.ml", line 543, characters 11-1023
Called from Constr_matching.sub_match.try_aux in file "pretyping/constr_matching.ml", line 646, characters 4-27
Called from Constr_matching.sub_match.aux.next in file "pretyping/constr_matching.ml", line 543, characters 11-1023
Called from Constr_matching.sub_match.try_aux in file "pretyping/constr_matching.ml", line 646, characters 4-27
Called from Constr_matching.sub_match.aux.next in file "pretyping/constr_matching.ml", line 543, characters 11-1023
Called from Constr_matching.sub_match.try_aux in file "pretyping/constr_matching.ml", line 646, characters 4-27
Called from Constr_matching.sub_match.aux.next in file "pretyping/constr_matching.ml", line 543, characters 11-1023
Called from Constr_matching.sub_match.try_aux in file "pretyping/constr_matching.ml", line 646, characters 4-27
Called from Constr_matching.sub_match.aux.next in file "pretyping/constr_matching.ml", line 543, characters 11-1023
Called from Constr_matching.sub_match.try_aux.try_sub_match_rec.next in file "pretyping/constr_matching.ml", line 643, characters 22-54
Called from Constr_matching.sub_match.aux.next in file "pretyping/constr_matching.ml", line 543, characters 11-1023
Called from Constr_matching.sub_match.try_aux in file "pretyping/constr_matching.ml", line 646, characters 4-27
Called from Constr_matching.sub_match.aux.next in file "pretyping/constr_matching.ml", line 543, characters 11-1023
Called from Constr_matching.sub_match.try_aux in file "pretyping/constr_matching.ml", line 646, characters 4-27
Called from Constr_matching.sub_match.aux.next in file "pretyping/constr_matching.ml", line 543, characters 11-1023
Called from Constr_matching.sub_match.try_aux in file "pretyping/constr_matching.ml", line 646, characters 4-27
Called from Constr_matching.sub_match.aux.next in file "pretyping/constr_matching.ml", line 543, characters 11-1023
Called from Constr_matching.sub_match.try_aux.try_sub_match_rec.next in file "pretyping/constr_matching.ml", line 643, characters 22-54
Called from Constr_matching.sub_match.try_aux.try_sub_match_rec.next in file "pretyping/constr_matching.ml", line 643, characters 22-54
Called from Constr_matching.sub_match.try_aux.try_sub_match_rec.next in file "pretyping/constr_matching.ml", line 643, characters 22-54
Called from Constr_matching.sub_match.aux.next in file "pretyping/constr_matching.ml", line 543, characters 11-1023
Called from Constr_matching.sub_match.try_aux.try_sub_match_rec.next in file "pretyping/constr_matching.ml", line 643, characters 22-54
Called from Constr_matching.sub_match.try_aux.try_sub_match_rec.next in file "pretyping/constr_matching.ml", line 643, characters 22-54
Called from Constr_matching.sub_match.try_aux.try_sub_match_rec.next in file "pretyping/constr_matching.ml", line 643, characters 22-54
Called from Constr_matching.sub_match.try_aux.try_sub_match_rec.next in file "pretyping/constr_matching.ml", line 643, characters 22-54
Called from Constr_matching.sub_match.try_aux.try_sub_match_rec.next in file "pretyping/constr_matching.ml", line 643, characters 22-54
Called from Constr_matching.sub_match.try_aux.try_sub_match_rec.next in file "pretyping/constr_matching.ml", line 643, characters 22-54
Called from Constr_matching.sub_match.aux.next in file "pretyping/constr_matching.ml", line 543, characters 11-1023
Called from Constr_matching.sub_match.try_aux.try_sub_match_rec.next in file "pretyping/constr_matching.ml", line 643, characters 22-54
Called from Constr_matching.sub_match.try_aux.try_sub_match_rec.next in file "pretyping/constr_matching.ml", line 643, characters 22-54
Called from Constr_matching.sub_match.try_aux.try_sub_match_rec.next in file "pretyping/constr_matching.ml", line 643, characters 22-54
Called from Constr_matching.sub_match.try_aux.try_sub_match_rec.next in file "pretyping/constr_matching.ml", line 643, characters 22-54
Called from Constr_matching.sub_match.aux.next in file "pretyping/constr_matching.ml", line 543, characters 11-1023
Called from Constr_matching.sub_match.try_aux.try_sub_match_rec.next in file "pretyping/constr_matching.ml", line 643, characters 22-54
Called from Constr_matching.sub_match.try_aux.try_sub_match_rec.next in file "pretyping/constr_matching.ml", line 643, characters 22-54
Called from Constr_matching.sub_match.aux.next in file "pretyping/constr_matching.ml", line 543, characters 11-1023
Called from Constr_matching.sub_match.try_aux.try_sub_match_rec.next in file "pretyping/constr_matching.ml", line 643, characters 22-54
Called from Constr_matching.sub_match.try_aux.try_sub_match_rec.next in file "pretyping/constr_matching.ml", line 643, characters 22-54
Called from Constr_matching.sub_match.aux.next in file "pretyping/constr_matching.ml", line 543, characters 11-1023
Called from Constr_matching.sub_match.try_aux.try_sub_match_rec.next in file "pretyping/constr_matching.ml", line 643, characters 22-54
Called from Constr_matching.sub_match.try_aux.try_sub_match_rec.next in file "pretyping/constr_matching.ml", line 643, characters 22-54
Called from Constr_matching.sub_match.aux.next in file "pretyping/constr_matching.ml", line 543, characters 11-1023
Called from Constr_matching.sub_match.try_aux.try_sub_match_rec.next in file "pretyping/constr_matching.ml", line 643, characters 22-54
Called from Constr_matching.sub_match.aux.next in file "pretyping/constr_matching.ml", line 543, characters 11-1023
Called from Constr_matching.sub_match.try_aux in file "pretyping/constr_matching.ml", line 646, characters 4-27
Called from Constr_matching.sub_match.aux.next in file "pretyping/constr_matching.ml", line 543, characters 11-1023
Called from Constr_matching.sub_match.try_aux in file "pretyping/constr_matching.ml", line 646, characters 4-27
Called from Constr_matching.sub_match.aux.next in file "pretyping/constr_matching.ml", line 543, characters 11-1023
Called from Constr_matching.sub_match.try_aux in file "pretyping/constr_matching.ml", line 646, characters 4-27
Called from Constr_matching.sub_match.aux.next in file "pretyping/constr_matching.ml", line 543, characters 11-1023
Called from Constr_matching.sub_match.aux.next in file "pretyping/constr_matching.ml", line 543, characters 11-1023
Called from Constr_matching.sub_match.try_aux in file "pretyping/constr_matching.ml", line 646, characters 4-27
Called from Constr_matching.sub_match.aux.next in file "pretyping/constr_matching.ml", line 543, characters 11-1023
Called from Constr_matching.sub_match.try_aux.try_sub_match_rec.next in file "pretyping/constr_matching.ml", line 643, characters 22-54
Called from Constr_matching.sub_match.try_aux.try_sub_match_rec.next in file "pretyping/constr_matching.ml", line 643, characters 22-54
Called from Constr_matching.sub_match.aux.next in file "pretyping/constr_matching.ml", line 543, characters 11-1023
Called from Constr_matching.sub_match.try_aux.try_sub_match_rec.next in file "pretyping/constr_matching.ml", line 643, characters 22-54
Called from Constr_matching.sub_match.try_aux.try_sub_match_rec.next in file "pretyping/constr_matching.ml", line 643, characters 22-54
Called from Constr_matching.sub_match.aux.next in file "pretyping/constr_matching.ml", line 543, characters 11-1023
Called from Constr_matching.sub_match.try_aux.try_sub_match_rec.next in file "pretyping/constr_matching.ml", line 643, characters 22-54
Called from Constr_matching.sub_match.aux.next in file "pretyping/constr_matching.ml", line 543, characters 11-1023
Called from Constr_matching.sub_match.try_aux in file "pretyping/constr_matching.ml", line 646, characters 4-27
Called from Constr_matching.sub_match.aux.next in file "pretyping/constr_matching.ml", line 543, characters 11-1023
Called from Constr_matching.sub_match.try_aux in file "pretyping/constr_matching.ml", line 646, characters 4-27
Called from Constr_matching.sub_match.aux.next in file "pretyping/constr_matching.ml", line 543, characters 11-1023
Called from Constr_matching.sub_match.try_aux in file "pretyping/constr_matching.ml", line 646, characters 4-27
Called from Constr_matching.sub_match.aux.next in file "pretyping/constr_matching.ml", line 543, characters 11-1023
Called from Constr_matching.sub_match.aux.next in file "pretyping/constr_matching.ml", line 543, characters 11-1023
Called from Constr_matching.sub_match.try_aux.try_sub_match_rec.next in file "pretyping/constr_matching.ml", line 643, characters 22-54
Called from Constr_matching.sub_match.try_aux.try_sub_match_rec.next in file "pretyping/constr_matching.ml", line 643, characters 22-54
regarding the directory stuff: I see the sequence:
1 caml_c_call (in coqc) + 28 [0x104f6feb8]
+ 1 caml_sys_read_directory (in coqc) + 144 [0x104f60bcc] sys.c:683
+ 1 caml_read_directory (in coqc) + 40 [0x104f64178] unix.c:345
+ 1 readdir (in libsystem_c.dylib) + 44 [0x1954d3370]
+ 1 _readdir_unlocked (in libsystem_c.dylib) + 152 [0x1954d323c]
+ 1 ??? (in <unknown binary>) [0x106c68380]
+ 1 caml_c_call (in coqc) + 28 [0x104f6feb8]
+ 1 caml_sys_read_directory (in coqc) + 144 [0x104f60bcc] sys.c:683
+ 1 caml_read_directory (in coqc) + 40 [0x104f64178] unix.c:345
+ 1 readdir (in libsystem_c.dylib) + 44 [0x1954d3370]
+ 1 _readdir_unlocked (in libsystem_c.dylib) + 152 [0x1954d323c]
+ 1 ??? (in <unknown binary>) [0x106c68380]
+ 1 caml_c_call (in coqc) + 28 [0x104f6feb8]
nested about 500 function levels deep - unlikely to be the cause for a 64M stack overflow, but still a bit strange.
@herbelin : I tried:
Search (?x * ?y).
Search (?x * ?y = ?y * ?x).
Both also result in a stack overflow.
This does work, though:
Search "assoc".
OK, this is consistent with the trace that says that it is a "loop" in the pattern-matching algorithm (file constr_matching.ml
).
One would need to see on which exact pattern-matching problem it explodes but a "very long computation" is not to be excluded.
I assumed that the Search
pattern has to match the searched lemmas without any reductions done on either side - just pattern variables on the pattern side and quantified variables on the lemma side can be assigned. Is this not so? Does Search
use full unification of the pattern and the searched lemma statements?
I'll have a look.
You're right, "long computation" does not make sense here.
If I put a Search (?x + 0 = ?x).
at the end of IdentifiersLibrary.v
, it works for me. If I put it at the beginning of a file which imports IdentifiersLibrary.v
(e.g. IdentifiersGenerate.v
), it works.
Could it be an OCaml bug in implementing tail recursion on M1/M2? Constr_matching.sub_match
is supposed to be tail-recursive, so you should not have the trace above.
Possibly it is an OCaml issue. Still a 64M stack overflow for a simple search is strange - isn't it? What is it doing?
Search
is matching the expression against all subterms of a statement. Without tail recursion optimization, it stacks several calls for each node of the statement (each next
in the backtrace log corresponds to a new node). IdentifiersLibrary.v
has very large statements (relying on notations hiding the complexity), so that seems plausible to exhaust the stack.
I see. Who follows up on the OCaml question?
In case it is really an issue with TRO on ARM, I would suggest to patch away the search and document in the release notes that there is such an issue on ARM.
I see. Who follows up on the OCaml question?
I have no idea. I don't know if the problem has been reported. A search for "tail" and "Apple" on the OCaml bug tracker gives nothing recent.
I would suggest to patch away the search and document in the release notes that there is such an issue on ARM.
You mean in rewriter
?
I mean we patch away the Search in rewriter and document in the release notes of Coq / Coq Platform that there might be an issue with Search (and possibly other things).
Who in the Coq team has the best connections to the OCaml maintainers?
@gadmm might know something about this
Incidentally, it is probably unrelated because next
above has only one argument, but I just learnt that tail recursion optimization in OCaml is limited by the number of registers (in particular only for functions with less than 10 arguments on x86).
Added: this information seems actually obsolete since 4.14.0 (OCaml PR 19595) and the limit was 6 + 10 IIUC.
Actually, I'm using ocaml 4.14.1 (installed with opam) and the detected architecture is arm64, so the same as you, I guess. As said, the Search
example works for me. I double-checked that tail call optimization is active for constr matching for me.
Are you compiling ocaml with special flags?
I am using a plain OCaml 4.13.1. Possibly I should switch to 4.14.1.
ocaml/ocaml#10595 is relevant in lifting arbitrary restrictions on TCO. I suggest adding @tailcall
attributes in tail recursive function applications to attest that it is a bug in Coq.
Some good news: I switched to OCaml 4.14.1 and rewriter 0.0.7 compiles fine with it without any hacks.
So shall we conclude that this was an early OCaml for ARM artefact and we can close this?
So shall we conclude that this was an early OCaml for ARM artefact and we can close this?
I would say so. Maybe indeed related to ocaml/ocaml#10595 which landed in 4.14.0.
In this case is it not still a bug in Coq (unless minimal OCaml version requirement is increased to 4.14)?
Well OCaml for ARM is still slightly experimental and I think it is known that for ARM a later OCaml version works better. My plan was to document it in the Coq Platform release notes. Also Coq Platform is tied to 4.14.1 now.
I am not sure if it is easy to make an ARM specific version restriction on OCaml in opam.
I am not sure if it is easy to make an ARM specific version restriction on OCaml in opam.
I can probably copy CompCert and do something like
"ocaml" {>= "4.14.0" | (arch != "arm64" & arch != "aarch64")}
Does this look right?
Yes, this looks right, but for platform it is not required since it is anyway tied to OCaml 4.14.1. Still it makes sense to do this.
I just tried to compile version 0.0.7 on an ARM / Apple silicon Mac. the maximum stack size one can specify on macOS is 64MB. This is sufficient to compile version 0.0.6, but it is not sufficient for 0.0.7.