This repository was archived by the owner on Apr 26, 2025. It is now read-only.
This repository was archived by the owner on Apr 26, 2025. It is now read-only.
Write / Restore State incompatible with native compilation #2
Description
Definition b := true.
Write State "foo_state".
Restore State "foo_state".
cannot find file /home/mdenes/native-coq/kernel/foo_state.coq.cmxs in search path
Eval native_compute in b.
Compilation...
File "/tmp/Coq_native6784ac.ml", line 6, characters 2-14:
Error: Unbound value const_NTop_b
Anomaly: Compilation failure. Please report.