search

ccz181078 / Coq-BB5

156 stars 6 forks source link

Proof hangs while compiling BB52Theorem.vo #8

Open sligocki opened 1 week ago

sligocki commented 1 week ago

I'm having a problem compiling since the switch to coqnative. This is on Mac, simply running make in root dir. It seems to "finish" (printing Axioms used) in the expected amount of time, but then just hangs for hours until eventually I Ctrl-C to kill it. Will try updating my ulimit.

time make
/Applications/Xcode.app/Contents/Developer/usr/bin/make -C BusyCoq/.
make[3]: Nothing to be done for `real-all'.
/Applications/Xcode.app/Contents/Developer/usr/bin/make -C CoqBB5/.
COQC BB52Theorem.v
Finished transaction in 4.344 secs (4.27u,0.068s) (successful)
ld: warning: -undefined suppress is deprecated
ld: warning: -undefined suppress is deprecated
...
ld: warning: -undefined suppress is deprecated
ld: warning: -undefined suppress is deprecated
Finished transaction in 112.495 secs (1.577u,0.239s) (successful)
Axioms:
functional_extensionality_dep
  : forall (A : Type) (B : A -> Type) (f g : forall x : A, B x),
    (forall x : A, f x = g x) -> f = g
COQNATIVE BB52Theorem.vo
^Cmake[3]: *** Deleting file `BB52Theorem.vo'
make[3]: *** [BB52Theorem.vo] Interrupt: 2
make[2]: *** [all] Interrupt: 2
make[1]: *** [all] Interrupt: 2
make: *** [CoqBB5/.] Interrupt: 2

make  10092.93s user 67.84s system 73% cpu 3:49:41.30 total
clang: error: unable to execute command: Interrupt: 2
clang: error: clang integrated assembler command failed due to signal (use -v to see invocation)
Apple clang version 16.0.0 (clang-1600.0.26.4)
Target: x86_64-apple-darwin23.6.0
Thread model: posix
InstalledDir: /Applications/Xcode.app/Contents/Developer/Toolchains/XcodeDefault.xctoolchain/usr/bin
clang: note: diagnostic msg:
********************

PLEASE ATTACH THE FOLLOWING FILES TO THE BUG REPORT:
Preprocessed source(s) and associated run script(s) are located at:
clang: note: diagnostic msg: /var/folders/88/6s9dyd8x3438m3fk7r3240c910v55q/T/camlasm60fdb2-15b496.S
clang: note: diagnostic msg: /var/folders/88/6s9dyd8x3438m3fk7r3240c910v55q/T/camlasm60fdb2-15b496.sh
clang: note: diagnostic msg: Crash backtrace is located in
clang: note: diagnostic msg: /Users/sl929/Library/Logs/DiagnosticReports/clang_<YYYY-MM-DD-HHMMSS>_<hostname>.crash
clang: note: diagnostic msg: (choose the .crash file that corresponds to your crash)
clang: note: diagnostic msg:

********************
File "./.coq-native/NCoqBB5_BB52Theorem.native", line 1:
Error: Assembler error, input left in file /var/folders/88/6s9dyd8x3438m3fk7r3240c910v55q/T/camlasm60fdb2.s
sligocki commented 1 week ago

I'm seeing the same hang after running ulimit -s unlimited which has been stuck for about 3hrs at the same spot as above:

Finished transaction in 130.791 secs (1.887u,0.295s) (successful)
Axioms:
functional_extensionality_dep
  : forall (A : Type) (B : A -> Type) (f g : forall x : A, B x),
    (forall x : A, f x = g x) -> f = g
COQNATIVE BB52Theorem.vo

I noticed that there's a clang job in my activity monitor that is using 100% (of one) core and has been running for 3hr as well. I'll let it run for a while longer and see if anything changes.

sligocki commented 1 week ago

Hm, it finally finished after 12 hours. Is this expected or does it finish faster for y'all after the coqnative update?

tcosmo commented 1 week ago

It does not hang on my system and finishes right about the axiom print.

Maybe @SkySkimmer knows?

SkySkimmer commented 1 week ago

I did say

The main problem which prevented me making a PR was coqnative crashing with stack overflow when trying to compile the resulting vo.

in #7

It may work to put the computation in an opaque module, ie instead of the current


Definition q0 := root_q_upd1_simplified.

Definition q_suc:SearchQueue->SearchQueue := (fun x => SearchQueue_upds x decider_all 20).

Definition q_0 := q0.

Definition q_1_def := q_suc q_0.
Time Definition q_1 := Eval native_compute in q_1_def.
(* ... *)

Definition q_200_def := q_suc q_199.
Time Definition q_200 := Eval native_compute in q_200_def.

Lemma iter_S{A}(f:A->A)(x x0:A) n:
  x0 = Nat.iter n f x ->
  f x0 = Nat.iter (S n) f x.
Proof.
  intro H.
  rewrite H.
  reflexivity.
Qed.

Ltac q_rw q_x q_x_def :=
  assert (H:q_x = q_x_def) by (native_cast_no_check (eq_refl q_x));
  rewrite H; unfold q_x_def; clear H; apply iter_S.

Lemma q_200_spec: q_200 = Nat.iter 200 q_suc q_0.
(* ... *)
Qed.

Lemma q_200_WF:
  SearchQueue_WF (N.to_nat BB5_minus_one) q_200 root.
Proof.
(* ... *)
Qed.

Lemma q_200_empty:
  q_200 = (nil,nil).
Proof.
reflexivity.
Qed.

you would do

Module Type BigComputeT.
  Parameter WF_empty : SearchQueue_WF (N.to_nat BB5_minus_one) (nil,nil) root.
End BigComputeT.

(* Opaque module prevents native compilation of the contents *)
Module BigCompute : BigComputeT.

Definition q0 := root_q_upd1_simplified.

Definition q_suc:SearchQueue->SearchQueue := (fun x => SearchQueue_upds x decider_all 20).

Definition q_0 := q0.

Definition q_1_def := q_suc q_0.
Time Definition q_1 := Eval native_compute in q_1_def.
(* ... *)

Definition q_200_def := q_suc q_199.
Time Definition q_200 := Eval native_compute in q_200_def.

Lemma iter_S{A}(f:A->A)(x x0:A) n:
  x0 = Nat.iter n f x ->
  f x0 = Nat.iter (S n) f x.
Proof.
  intro H.
  rewrite H.
  reflexivity.
Qed.

Ltac q_rw q_x q_x_def :=
  assert (H:q_x = q_x_def) by (native_cast_no_check (eq_refl q_x));
  rewrite H; unfold q_x_def; clear H; apply iter_S.

Lemma q_200_spec: q_200 = Nat.iter 200 q_suc q_0.
(* ... *)
Qed.

Lemma q_200_empty:
  q_200 = (nil,nil).
Proof.
reflexivity.
Qed.

Lemma WF_empty:
  SearchQueue_WF (N.to_nat BB5_minus_one) (nil,nil) root.
rewrite <-q_200_empty.
(* ... *)
Qed.

End BigCompute.
tcosmo commented 1 week ago

coqnative crashing with stack overflow when trying to compile the resulting vo.

This does not seem to be what happens to everyone:

Note that even with vm_compute using coqchk on the .vo fails for an unknown reason.

In front of these issues we may either try what you are suggesting (although I have 0 expertise to implement/debug it) or go back to vm_compute but parallelize the proof, which is currently WIP (see https://github.com/ccz181078/Coq-BB5/commit/3a74388e237e2405d7fc50e77368e9092a1fe4e3).

Thank you!

sligocki commented 1 week ago

I guess that my experience now is no worse than it was before the switch to native compute, so I guess don't feel a need to rollback because of my experience. it is confusing since it's taking so long after proof completes, but I guess that's fine.