search

jwiegley / category-theory

An axiom-free formalization of category theory in Coq for personal study and practical work
BSD 3-Clause "New" or "Revised" License
745 stars 68 forks source link

Compatibility with Coq 8.8? #11

Closed langston-barrett closed 5 years ago

langston-barrett commented 6 years ago

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 commented 6 years ago

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 commented 6 years ago

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 commented 6 years ago

Okay, thanks for getting back to me so quickly!

jwiegley commented 6 years ago

@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 commented 6 years ago

Logged as https://github.com/coq/coq/issues/8004

JasonGross commented 6 years ago

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 commented 6 years ago

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

jwiegley commented 5 years ago

8.8 is now supported.