The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

How can I compile git AT github.com:mattam82/coq.git?  When I run `./configure -no-native-compiler -prefix "$HOME/.local64/coq/coq-univpolyproj/"` and then `make -j16 -k` and then I run `make -j16 -k` again, I get

$ make -j16 -k

make --warn-undefined-variable --no-builtin-rules -f Makefile.build "world"

make[1]: Entering directory `/afs/csail.mit.edu/u/j/jgross/coq-univpolyproj'

CHECK revision

OCAMLOPT  kernel/term_typing.ml

OCAMLC    kernel/term_typing.ml

./doc/stdlib/make-library-index doc/stdlib/index-list.html doc/stdlib/hidden-files

File "kernel/term_typing.ml", line 31, characters 32-33:

Error: This _expression_ has type Environ.unsafe_judgment

       but an _expression_ was expected of type Term.constr = Constr.t

make[1]: *** [kernel/term_typing.cmx] Error 2

Building file index-list.prehtml ...theories/Arith

File "kernel/term_typing.ml", line 31, characters 32-33:

Error: This _expression_ has type Environ.unsafe_judgment

       but an _expression_ was expected of type Term.constr = Constr.t

make[1]: *** [kernel/term_typing.cmo] Error 2

theories/Bool

theories/Classes

Error: none of doc/stdlib/index-list.html and doc/stdlib/hidden-files mention theories/Classes/CEquivalence.v

make[1]: *** [doc/stdlib/index-list.html] Error 1

make[1]: Target `world' not remade because of errors.

make[1]: Leaving directory `/afs/csail.mit.edu/u/j/jgross/coq-univpolyproj'

make: *** [world] Error 2

make: Target `NOARG' not remade because of errors.

Thanks,

Jason

On Friday, September 6, 2013, Matthieu Sozeau wrote:

On 6 sept. 2013, at 01:07, vincent rahli <vincent.rahli AT gmail.com> wrote:

> Hi,
>
> We're trying to use the HoTT branch of Coq (downloaded today) in order to get
> universe polymorphism.
>
> Unfortunately we keep on running into this error [Error: Universe inconsistency],
> which is the very error we were trying to avoid by using the HoTT branch of Coq.
>
> One of our problems is that [try] does not catch this error (see the code below).
>
>   - Why doesn't [try] catch that error?
>   - Why do we get a universe inconsistency error here and not
>     [Error: Unable to unify.] (without the [try])?

Hi,

  Indeed that version of unification didn't turn inconsistencies into unification
failures. The current development version [1] fixes this, I hope to push it to the
HoTT/coq repository soon. The proof goes through though if you avoid this step:

Proof.
induction sub; simpl; intros.
destruct H.
simpl in IHsub.
split; try right; (apply (IHsub vars);
destruct a, sub; [apply X| destruct p; apply X]).
Qed.

  Also, as a workaround, putting NTerm in [Set] where it naturally falls gets rid
of the inconsistency.

[1] git AT github.com:mattam82/coq.git branch univpolyproj

Best,
-- Matthieu

> Thanks.
> Vincent & Abhishek.
>
> -----------------------------------------------------------------------------------------
>
> Require Export Coq.Lists.List.
>
> Polymorphic Fixpoint LIn (A : Type) (a:A) (l:list A) : Type :=
>   match l with
>     | nil => False
>     | b :: m => (b = a) + LIn A a m
>   end.
>
> Polymorphic Inductive NTerm : Type :=
> | cterm : NTerm
> | oterm : list NTerm -> NTerm.
>
> Polymorphic Fixpoint dummy {A B} (x : list (A * B)) : list (A * B) :=
>   match x with
>     | nil => nil
>     | (_, _) :: _ => nil
>   end.
>
> Lemma foo :
>   forall v t sub vars,
>     LIn (nat * NTerm) (v, t) (dummy sub)
>     ->
>     (
>       LIn (nat * NTerm) (v, t) sub
>       *
>       notT (LIn nat v vars)
>     ).
> Proof.
>   induction sub; simpl; intros.
>   destruct H.
>   try (apply IHsub in X).
>