search

coq / coq

Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.
https://coq.inria.fr/
GNU Lesser General Public License v2.1
4.72k stars 637 forks source link

`lia` cache should not use OCaml type-unsafe marshalling functions #10957

Open robbertkrebbers opened 4 years ago

robbertkrebbers commented 4 years ago 
Require Import Psatz Fin.

Fixpoint fin_to_nat {n} (i : Fin.t n) : nat :=
  match i with F1 => 0 | FS i => S (fin_to_nat i) end.

Lemma foo (n : nat) (i : Fin.t n) :
  0 = S (fin_to_nat i) ->
  F1 = FS i.
Proof. lia. (* segmentation fault *)

Coq Version

Using Coq master 6ed3b02af77313d62ec868b4a88a208a9003857d

$ coqtop -v
The Coq Proof Assistant, version 8.11+alpha (October 2019)
compiled on Oct 25 2019 9:04:16 with OCaml 4.05.0
mattam82 commented 4 years ago

Is that a regression?

robbertkrebbers commented 4 years ago

Yes, it works with 8.10.1

ppedrot commented 4 years ago

I cannot reproduce on 6ed3b02af77313d62ec868b4a88a208a9003857d with OCaml 4.06.1+fp.

robbertkrebbers commented 4 years ago

I'm using:

$ ocaml --version
The OCaml toplevel, version 4.05.0
robbertkrebbers commented 4 years ago

This issue is kind of a blocker for me. Debian testing ships OCaml 4.05.0, so it's impossible to build Coq master now.

ppedrot commented 4 years ago

Still cannot reproduce on the same commit and using the 4.05.0 OCaml compiler shipped with Debian. Did you try from a fresh install?

ppedrot commented 4 years ago

Relevant for this kind of problem:

pm@ouranos:~/sources/coq$ ulimit -s
8192
robbertkrebbers commented 4 years ago

It appears to have something to do with my .lia.cache. I removed that file (which was created by an older version of Coq), and now lia works again without segfaulting.

I still think this is a bug, since coqc should never segfault.

silene commented 4 years ago

"never" is too strong a word. As @ppedrot mentioned, a resource shortage (either stack or heap) is a perfectly fine segfault.

ppedrot commented 4 years ago

@robbertkrebbers This is most likely caused by the fact that lia uses the OCaml marshalling functions, which are type-unsound. Changing the title accordingly.

ejgallego commented 4 years ago

Indeed a different serialization method could help, but as a short term fix a magic number could help avoid these kind of problems.

ppedrot commented 4 years ago

I think it's fairly easy to remove the need to OCaml marshaller, I'll write a quick patch.

maximedenes commented 4 years ago

@ppedrot any update?

ppedrot commented 4 years ago

@maximedenes nope, it's simple but tedious to write the marshallers and I am lazy.

maximedenes commented 3 years ago

@ppedrot do you need to be forced? ;)