Compatibility with Coq 8.8?

[langston-barrett]

Hi, I'm trying to update the version of this library in nixpkgs, but when I add the following lines to the default.nix there:

    "8.8" = {
      version = "20180705";
      rev = "2685dc91f528dc3e82f17a1c32804a94d2ee8ed7";
      sha256 = "0ll22lfzjglnvvf4p0vwk8crwn2c5lkawd85wr3qzcrwnpp5dc43";
    };

and

    compatibleCoqVersions = v: builtins.elem v [ "8.6" "8.7" "8.8" ];

I get this error when building:

File "./Lib/Nomega.v", line 92, characters 2-21:
Warning: Nge is N.ge [compatibility-notation,deprecated]
COQC Lib/Tactics.v
COQC Lib/Datatypes.v
COQC Lib/Equality.v
Closed under the global context
     = tt
     : typeD (fun _ : type => unit) Ty
     = 5
     : typeD (fun _ : type => nat) Ty
File "./Lib/Datatypes.v", line 212, characters 0-4:
Error:
Illegal application:
The term "list_equivalence_obligation_1" of type
 "∀ (A : Type) (H : Setoid A), Reflexive list_equiv"
cannot be applied to the terms
 "A" : "Type"
 "H" : "Setoid A"
The 1st term has type "Type@{Category.Lib.Datatypes.1007}"
which should be coercible to "Type@{Category.Lib.Datatypes.1020}".

Is this library compatible with Coq 8.8?

[jwiegley]

It is not compatible yet. I have an item on my own private task list to report some bugs against the Coq tracker for things like the above. It's not that hard to move past the issue you're seeing now by defining the body of the list equivalence separately, but then you'll just run into another anamoly a bit further down the file.

[jwiegley]

I'm still using Coq 8.7 for all my uses of this library, but I think that moving to 8.8 should become a priority now.

[langston-barrett]

Okay, thanks for getting back to me so quickly!

[jwiegley]

@siddharthist I'm more interrupt driven than I like to think, but your questions have prompted me to create those bugs today. Running the bug minifier now, and will update this issue to point to the Coq bug once created.

[jwiegley]

Logged as coq/coq#8004

[JasonGross]

Once you get this working with 8.8 / master, you should add it to Coq's CI so that it doesn't accidentally break.

[jwiegley]

@JasonGross How does one add something to Coq's CI?

[jwiegley]

8.8 is now supported.