The following code overflows the stack.

From Unicoq Require Import Unicoq.
Polymorphic Record dyn : Prop := mkdyn {}.
Polymorphic Definition Dyn {A} (a:A) : dyn. constructor. Qed.
Check ltac:(munify Dyn@{Set} Dyn@{Type}; exact tt).

I can't seem to get this repository to build against 8.11.0. I checked out:c33e66c8f2924449c7b98aab108d97b5ee105bab per @Janno 's suggestion but i still get the following.

$ make -j3
CAMLDEP src/munify.ml
coq_makefile -f Make -o Makefile
CAMLOPT -c -for-pack Unicoq src/munify.ml
CAMLOPT -c -for-pack Unicoq src/unitactics.ml
CAMLOPT -pack -o src/unicoq.cmx
CAMLOPT -a -o src/unicoq.cmxa
CAMLOPT -shared -o src/unicoq.cmxs
COQC theories/Unicoq.v
File "./theories/Unicoq.v", line 7, characters 0-27:
Error: while loading
/home/gmalecha/bedrock/mtac-testing/unicoq/src/unicoq.cmxs:
The module `Int_misc' is already loaded (either by the main program or a previously-dynlinked library)

make[1]: *** [Makefile:678: theories/Unicoq.vo] Error 1
make: *** [Makefile:327: all] Error 2

CAMLC -c src/munify.mli
File "src/munify.mli", line 6, characters 18-33:
Error: Unbound module Big_int
make[1]: *** [Makefile:584: src/munify.cmi] Error 2

NB: the num library is installed, but the build-system does not look for it.

The Coq team released Coq 8.15.0 on January 13, 2022.
The corresponding Coq Platform release 2022.02 should be released before February 28, 2022.
It can be delayed in case of difficulties until April 11, 2022, but this should be an exception.

This issue is to inform you that to our (possibly a few days old) best knoweldege the latest released version of your project (1.6+8.14) does not work with Coq 8.15.0.
We tried to remove version restrictions in opam files and possibly make or configure files, but this did not suffice.

Please note that in Coq Platform CI (unlike Coq CI) we test only released / tagged versions. Coq CI is currently testing commit 2095dff on repository https://github.com/unicoq/unicoq - which likely means that this commit does work in Coq CI.

Could you please create a tag and opam package, or communicate us any existing tag that works with Coq branch v8.15, preferably before February 14, 2022?
In case we might have to delay the Coq Platform release cause of issues with your project, we would prefer to be informed about the situation as early as possible.

In case the tag and opam package are available before January 25, 2022, it will be included in an early Coq Platform beta release of the for Coq 8.15.0.

The working branch of Coq Platform, which already supports Coq version 8.15.0, can be found here https://github.com/coq/platform/tree/main.

Please don't close this issue, even after creating the new tag and/or opam package.
We will close the issue after updating Coq Platform.
This is a measure of 'double book keeping' in order to avoid that we ship the wrong version.

In any case, Coq Platform won't be released before this issue is closed!

Thanks!

P.S.: this issue has been created automatically based on CI status.

CC: coq/platform#193

The compilation of the current version fails with:

CAMLOPT -c -for-pack Unicoq src/munify.ml
File "src/munify.ml", line 680, characters 8-32:
680 |         Termops.global_of_constr sigma t1, l1
              ^^^^^^^^^^^^^^^^^^^^^^^^
Alert deprecated: Termops.global_of_constr
Use [EConstr.destRef] instead (throws DestKO instead of Not_found).
File "src/munify.ml", line 682, characters 25-42:
682 |         let t1, r1 = try destProj sigma t1 with Constr.DestKO -> raise Not_found in
                               ^^^^^^^^^^^^^^^^^
Error: This expression has type
         Names.Projection.t * Sorts.relevance * EConstr.t
       but an expression was expected of type 'a * 'b

The algorithm now tries Meta-Inst, Meta-FO, Meta-DelDeps, etc. first in one direction and then all again in the other direction. It should try Meta-Inst both directons, Meta-FO both directions, and so on.

I am curious, what is the difference between the unification algorithm provided here vs the one Coq already has? What are some brief trade-offs and motivation for this one to exist in the first place?

Thanks in advance very interesting!

Despite my lack of involvement, two CS PRs I helped start were merged into Coq recently:

• coq/coq#14041 enabling projections on fun,
• coq/coq#14386 enabling projections dependent forall.

As far as I can tell, Unicoq needs to be adapted to support both of these.

(It does seem like the fixes might be very simple so I might be able to implement them soon. I'll post a draft PR as soon as I get to it. If there is no PR feel free to implement the changes!)

The Coq team is planning to release Coq 8.13-beta1 on December 7, 2020,
and Coq 8.13.0 on January 7, 2020.

Your project is currently scheduled for being bundled in the Windows installer.

We are currently testing commit 3dd7abd
on branch https://github.com/unicoq/unicoq/tree/master
but we would like to ship a released version instead (a tag in git's slang).

Could you please tag that commit, or communicate us any other tag
that works with the Coq branch v8.13 at the latest 15 days before the
date of the final release?

Thanks!
CC: coq/coq#12334

The Coq team released Coq 8.17+rc1 on December 29th, 2022 and plans to release Coq 8.17.0 around March 7th, 2023.
The corresponding Coq Platform release 2023.03 should be released before April 14th, 2023.
It can be delayed in case of difficulties until June 30, 2023, but this should be an exception.

This issue is to inform you that to our (possibly a few days old) best knowledge the latest released version of your project (1.6+8.16) does not work with Coq 8.17+rc1.
We tried to remove version restrictions in opam files and possibly make or configure files, but this did not suffice.

Please note that in Coq Platform CI (unlike Coq CI) we test only released / tagged versions. Coq CI is currently testing commit 0c33033 on repository https://github.com/unicoq/unicoq - which likely means that this commit does work in Coq CI.

Could you please create a tag and opam package, or communicate us any existing tag that works with Coq branch v8.17, preferably before March 21st, 2023?
In case we might have to delay the Coq Platform release cause of issues with your project, we would prefer to be informed about the situation as early as possible.

In case the tag and opam package are available before March 21st, 2023, it will be included in an early Coq Platform beta release of the for Coq 8.17+rc1.

The working branch of Coq Platform, can be found here main.
It contains package pick ~8.17~2023.03+preview1 which already supports Coq version 8.17+rc1 and contains already working (possibly patched / commit pinned) Coq Platform packages.

Please don't close this issue, even after creating the new tag and/or opam package.
We will close the issue after updating Coq Platform.
This is a measure of 'double book keeping' in order to avoid that we ship the wrong version.

In any case, Coq Platform won't be released before this issue is closed!

Thanks!

P.S.: this issue has been created automatically based on CI status.

CC: coq/platform#335

I see you already have merged quite a few things for Coq 8.18 compatibility, but you haven't formally tagged a release.

When will you do so?

Currently the metacoq branch is the one being actually developed. We need to clean up and make that one the official 1.1 version.

After a break of 6 weeks cause or branch restructuring I did rerun the Coq Platform Dev CI yesterday and I have issues compiling the UniCoq dev opam package, as far as I can tell so far only on Windows:

2021-04-18T20:43:34.7309771Z C:/cygwin_coq_platform/home/runneradmin/.opam/log/coq-unicoq-5632-d85068.out
2021-04-18T20:43:34.7434465Z      1	COQDEP VFILES
2021-04-18T20:43:34.7435420Z      2	COQPP src/unitactics.mlg
2021-04-18T20:43:34.7437559Z      3	CAMLDEP src/munify.mli
2021-04-18T20:43:34.7442436Z      4	CAMLDEP src/logger.mli
2021-04-18T20:43:34.7444874Z      5	OCAMLLIBDEP src/unicoq.mlpack
2021-04-18T20:43:34.7466763Z      6	CAMLDEP src/munify.ml
2021-04-18T20:43:34.7467449Z      7	CAMLDEP src/logger.ml
2021-04-18T20:43:34.7467951Z      8	CAMLDEP src/unitactics.ml
2021-04-18T20:43:34.7468454Z      9	CAMLC -c src/logger.mli
2021-04-18T20:43:34.7469002Z     10	File "src/logger.mli", line 6, characters 26-43:
2021-04-18T20:43:34.7469579Z     11	Error: Unbound module Reduction
2021-04-18T20:43:34.7470262Z     12	make[1]: *** [Makefile:655: src/logger.cmi] Error 2
2021-04-18T20:43:34.7470812Z     13	make: *** [Makefile:344: all] Error 2

In case you have seen this before, I would appreciate a hint. Where does the missing "Reduction" module come from?

As far as I can tell the only place where we unify primitive projections is in

I don't know how to best fix this. On the one hand we could change app_fo but it would need changes to its signature to deal with the (prim, const)/(const, prim) cases. On the other hand, I am hesitant to let reduction take care of it unless we can make sure to reduce the const side first.

Any ideas?

Here's a test case. I only tried this on master-8.11 but that has the same prim. projection patches as master:

From Unicoq Require Import Unicoq.

Set Primitive Projections.
Module M.
  Record bla := { c :> Type;  goal : c -> c -> Prop }.
  Arguments goal {_}.
End M.
Import M.

Ltac IHateLtac B k :=
    let ep := fresh "p" in
    let eq := fresh "q" in
    evar (ep : c B);
    evar (eq : c B);
    let p := eval unfold ep in ep in
    let q := eval unfold eq in eq in
    k p q; clear ep eq.

Section Test.
  Context (B : bla) (P Q : B).

  Set Printing Primitive Projection Parameters.

  Goal B.(@goal) P Q.
    (* Everything is phrased in terms of the constant [goal]. *)
    IHateLtac B ltac:(fun p q =>
      match goal with
      | |- ?g =>
        unify g (@goal B p q)
      end
    ).

    IHateLtac B ltac:(fun p q =>
      match goal with
      | |- ?g =>
        munify g (@goal B p q)
      end
    ).

    (* Let's make the RHS primitive *)

    (* [unify] doesn't care and succeeds *)
    IHateLtac B ltac:(fun p q =>
      match goal with
      | |- ?g =>
        let t := constr:(@goal B) in
        let t := eval unfold goal in t in
        is_proj t;
        unify g (t p q)
      end
    ).

    (* [munify] fails *)
    IHateLtac B ltac:(fun p q =>
      match goal with
      | |- ?g =>
        let t := constr:(@goal B) in
        let t := eval unfold goal in t in
        is_proj t;
        assert_fails (munify g (t p q))
      end
    ).

    progress unfold goal.
    (* goal is now a primitive projection. *)

    (* [unify] still does the right thing. *)
    IHateLtac B ltac:(fun p q =>
      match goal with
      | |- ?g =>
        unify g (@goal B p q)
      end
    ).

    (* [munify] fails *)
    IHateLtac B ltac:(fun p q =>
      match goal with
      | |- ?g =>
        assert_fails (munify g (@goal B p q))
      end
    ).

  Abort.

End Test.

The Coq team released Coq 8.16+rc1 on June 01, 2022.
The corresponding Coq Platform release 2022.09 should be released before September 15, 2022.
It can be delayed in case of difficulties until October 15, 2022, but this should be an exception.

This issue is to inform you that to our (possibly a few days old) best knowledge the latest released version of your project (preview) does not work with Coq 8.16+rc1.
We tried to remove version restrictions in opam files and possibly make or configure files, but this did not suffice.

Please note that in Coq Platform CI (unlike Coq CI) we test only released / tagged versions. Coq CI is currently testing commit 98beb32 on repository https://github.com/unicoq/unicoq - which likely means that this commit does work in Coq CI.

Could you please create a tag and opam package, or communicate us any existing tag that works with Coq branch v8.16, preferably before August 31, 2022?
In case we might have to delay the Coq Platform release cause of issues with your project, we would prefer to be informed about the situation as early as possible.

In case the tag and opam package are available before August 17, 2022, it will be included in an early Coq Platform beta release of the for Coq 8.16+rc1.

The working branch of Coq Platform, can be found here main.
It contains package pick ~8.16+rc1~2022.09~preview1 which already supports Coq version 8.16+rc1 and contains already working (possibly patched / commit pinned) Coq Platform packages.

Please don't close this issue, even after creating the new tag and/or opam package.
We will close the issue after updating Coq Platform.
This is a measure of 'double book keeping' in order to avoid that we ship the wrong version.

In any case, Coq Platform won't be released before this issue is closed!

Thanks!

P.S.: this issue has been created automatically based on CI status.

CC: coq/platform#274

Building constrs is very expensive for universe polymorphic contrs. It is my understanding that, in practice, lift has to be some kind of global name anyways (definition, inductive, etc.) It would be much cheaper to hard code this assumption by taking a global_reference instead of a builder function for a constr. is_lift could then call Nametab.is_global to compare the given term with the registered lift costant.

The Coq team released Coq 8.14+rc1 on September 17, 2021
and plans to release Coq 8.14.0 before October 31, 2021.
A corresponding Coq Platform releases should be released before November 30, 2021.
It can be dealyed in case of difficulties until January 31, 2022, but this should be an exception.

Coq CI is currently testing commit 5ed1cdf
on branch https://github.com/unicoq/unicoq/tree/master
but we would like to ship a released version instead (a tag in git's slang).

Coq Platform is currently not testing this package!

Could you please create a tag, or communicate us any existing tag that works with
Coq branch v8.14, preferably 15 days before November 30, 2021
or earlier? In case we might have to delay the Coq Platform release cause of issues with
your project, we would prefer to be informed about the situation as early as possible.

Thanks!

P.S.: this issue has been creates semi-automatically.

CC: coq/platform#139

The Coq team released Coq 8.19.0 on January 24th, 2024.
The corresponding Coq Platform release 2024.01 should be released before April 30th, 2024.
It can be delayed in case of difficulties until May 15th, 2024, but this should be an exception.

This issue is to inform you that to our (possibly a few days old) best knowledge the latest released version of your project (1.6+8.18) does not work with Coq 8.19.0.
We tried to remove version restrictions in opam files and possibly make or configure files, but this did not suffice.

Please note that in Coq Platform CI (unlike Coq CI) we test only released / tagged versions. Coq CI is currently testing commit e0486d2 on repository https://github.com/unicoq/unicoq - which likely means that this commit does work in Coq CI.

Could you please create a tag and opam package, or communicate us any existing tag that works with Coq branch v8.19, preferably before March 31st, 2024?
In case we might have to delay the Coq Platform release cause of issues with your project, we would prefer to be informed about the situation as early as possible.

In case the tag and opam package are available before March 31st, 2024, it will be included in an early Coq Platform beta release of the for Coq 8.19.0.

The working branch of Coq Platform, can be found here main.
It contains package pick ~8.19~2024.01+beta1 which already supports Coq version 8.19.0 and contains already working (possibly patched / commit pinned) Coq Platform packages.

Please don't close this issue, even after creating the new tag and/or opam package.
We will close the issue after updating Coq Platform.
This is a measure of 'double book keeping' in order to avoid that we ship the wrong version.

In any case, Coq Platform won't be released before this issue is closed!

Thanks!

P.S.: this issue has been created automatically based on CI status.

CC: coq/platform#405

The Coq team released Coq 8.18.0 on September 7th, 2023.
The corresponding Coq Platform release 2023.10 should be released before November 30th, 2023.
It can be delayed in case of difficulties until January 15th, 2023, but this should be an exception.

This issue is to inform you that the opam package we are currently testing in Coq Platform CI works fine with Coq 8.18.0.

Coq Platform CI is currently testing opam package coq-unicoq.1.6+8.18
from platform patch repository https://github.com/coq/platform/tree/main/opam/opam-coq-archive/released/packages/coq-unicoq/coq-unicoq.1.6+8.18/opam. This means we had to weaken some version restrictions in the opam package, but no other changes were required.

In case this is the version you want to see in Coq Platform, there is nothing to do for you - please just close this issue.

In case you would prefer to see an updated or an older version in the upcoming Coq Platform 2023.10, please inform us as soon as possible and before October 31st, 2023!

The working branch of Coq Platform, can be found here main.
It contains package pick ~8.18+beta1 which already supports Coq version 8.18.0 and contains already working (possibly patched / commit pinned) Coq Platform packages.

In case you want to select a different version, please don't close this issue, even after creating the new tag and/or opam package.
We will close the issue after updating Coq Platform.
This is a measure of 'double book keeping' in order to avoid that we ship the wrong version.

In any case, Coq Platform won't be released before this issue is closed!

Thanks!

P.S.: this issue has been created automatically based on CI status.

CC: coq/platform#372

It seems like the order in which variables are prunned is wrong, although I'm not sure. This has impact in Meta-DelDeps: is it removing the first or the last variables?

I wanted to get (or even print) the obvious unification substitution for:

(fun n : nat => ?Goal)

and

fun n : nat => eq_refl : 0 + n = n

How does one do this?

related: https://stackoverflow.com/questions/72924211/how-does-one-access-the-dependent-type-unification-algorithm-from-coqs-internal/73018218#73018218 and github.com/unicoq/unicoq/issues/69

This has been the case for a long time but we never opened an issue for it. Let's try to figure out what part of the Coq API would be useful here.

Hi,

I want to use this plugin for this coq (and coq-serapi) versions:

coq                     8.11.0        pinned to version 8.11.0
coq-serapi              8.11.0+0.11.0 pinned to version 8.11.0+0.11.0 at git+https://github.com/ejgallego/coq-serapi.git#v8.16

This came from trying out unicoq on coq/coq#6682. The code is:

Set Universe Polymorphism. Unset Universe Minimization ToSet.
Set Printing Universes.
Structure NoProof := no_proof { np_type : Type }.
Canonical Structure NP_Type := no_proof Type. 

From Unicoq Require Import Unicoq.
Set Use Unicoq.
Set Unicoq Debug.
Fail Definition A := (fun np (T : np_type np) => I) _ Type.

Unicoq correctly chooses NP_Type (this is where evarconv fails) but Unicoq neglects to insert the required universe constraints (as outlined in coq/coq#6682 (comment)).

I do not understand the code of check_conv_record enough to fix this myself.

Dear Unicoq Team,

since Unicoq has been part of the Windows installer since quite a while, I would like to include it into the Coq platform 8.11.2 and 8.12.0. I hope this matches your plans.

For this I would need your consent to include Mtac2 into the Coq platform, which is best expressed by creating an issue at https://github.com/MSoegtropIMC/coq-platform in which you state that you agree with the Coq platform charter at (https://github.com/MSoegtropIMC/coq-platform/blob/master/charter.md)

Unless you tell me otherwise, I would use the tags v1.3-8.11 and v1.4-8.12. As far as I can tell there are no opam packages for these tags. If you want, I can quickly create and push these for you.

Best regards,

Michael