coq-community / coqeal Goto Github PK

It seems wasteful and somewhat confusing to me to keep release archives (tarballs) in the releases directory in the repo itself.

The most obvious solution is to create GitHub releases with the proper tags and attaching the actual archives as binaries to each GitHub release.

@CoqEAL/coqeal I suggest to transfer this repository to coq-community, this could only increase the visibility and opportunities of maintenance.

Currently https://github.com/coq/opam-coq-archive/blob/master/released/packages/coq-coqeal/coq-coqeal.1.1.1/opam conflicts with 1.16

Error introduced by #27

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.1.1) 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 appears to test this project, but has some special handling for your project which makes it difficult to retrieve the commit it tests for your project.

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

The Coq team released Coq 8.14+rc1 on September 17, 2021 and plans to release Coq 8.14.0 before October 31, 2021.
The corresponding Coq Platform release 2021.11 should be released before November 30, 2021.
It can be delayed in case of difficulties until January 31, 2022, 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.14+rc1.

Coq Platform CI is currently testing opam package coq-coqeal.1.0.6
from official repository https://coq.inria.fr/opam/released/packages/coq-coqeal/coq-coqeal.1.0.6/opam.

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 2021.11, please inform us as soon as possible and before November 15, 2021!

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

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#139

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 the opam package we are currently testing in Coq Platform CI works fine with Coq 8.16+rc1.

Coq Platform CI is currently testing opam package coq-coqeal.1.1.1
from platform patch repository https://github.com/coq/platform/tree/main/opam/opam-coq-archive/released/packages/coq-coqeal/coq-coqeal.1.1.1/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 2022.09, please inform us as soon as possible and before August 31, 2022!

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.

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#274

For doing computation inside Coq using matrices, the most efficient way is likely as operations on Coq's primitive arrays. However, to make the connection to abstract MathComp matrices, there needs to be a refinement from them down to primitive arrays of arrays (e.g., via the refinement to lists of lists).

Suggested by a problem faced by @spitters.

Hi folks, I'm updating some old developments to CoqEAL , back in the day I used some branches such as paramcoq but now it seems that there are stale.

Maybe it'd be a good idea to clean these branches out?

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-coqeal.2.0.0
from official repository https://coq.inria.fr/opam/released/packages/coq-coqeal/coq-coqeal.2.0.0/opam.

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

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 the opam package we are currently testing in Coq Platform CI works fine with Coq 8.19.0.

Coq Platform CI is currently testing opam package coq-coqeal.2.0.1
from official repository https://coq.inria.fr/opam/released/packages/coq-coqeal/coq-coqeal.2.0.1/opam.

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 2024.01, please inform us as soon as possible and before March 31st, 2024!

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.

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#405

Hello,
in CoqEAL0.1, sorted_take (from ssrcomplements.v) had no transitivity assumption. In CoqEAL1.0.5, such an assumption exists. It may turn out be a problem one day.

export COQBIN=/usr/bin/
export SSRSRC=/home/martin/geo/CoqEAL/theory
export SSRLIB=/home/martin/geo/CoqEAL

nd in loadpath!
*** Warning: in file boolF2.v, library ssrbool.v is required and has not been found in loadpath!
*** Warning: in file boolF2.v, library eqtype.v is required and has not been found in loadpath!
*** Warning: in file boolF2.v, library ssrnat.v is required and has not been found in loadpath!
*** Warning: in file boolF2.v, library seq.v is required and has not been found in loadpath!
*** Warning: in file boolF2.v, library div.v is required and has not been found in loadpath!
*** Warning: in file boolF2.v, library choice.v is required and has not been found in loadpath!
*** Warning: in file boolF2.v, library fintype.v is required and has not been found in loadpath!
*** Warning: in file boolF2.v, library bigop.v is required and has not been found in loadpath!
*** Warning: in file boolF2.v, library finset.v is required and has not been found in loadpath!
*** Warning: in file boolF2.v, library prime.v is required and has not been found in loadpath!
*** Warning: in file boolF2.v, library fingroup.v is required and has not been found in loadpath!
*** Warning: in file boolF2.v, library ssralg.v is required and has not been found in loadpath!
*** Warning: in file boolF2.v, library zmodp.v is required and has not been found in loadpath!
*** Warning: in file boolF2.v, library finalg.v is required and has not been found in loadpath!
/usr/bin/coqdep -c -slash -I . "strassen.v" > "strassen.v.d" || ( RV=$?; rm -f "strassen.v.d"; exit ${RV} )
*** Warning: in file strassen.v, library Ncring.v is required and has not been found in loadpath!
*** Warning: in file strassen.v, library Ncring_tac.v is required and has not been found in loadpath!
*** Warning: in file strassen.v, library ssreflect.v is required and has not been found in loadpath!
*** Warning: in file strassen.v, library ssrbool.v is required and has not been found in loadpath!
*** Warning: in file strassen.v, library ssrfun.v is required and has not been found in loadpath!
*** Warning: in file strassen.v, library eqtype.v is required and has not been found in loadpath!
*** Warning: in file strassen.v, library ssrnat.v is required and has not been found in loadpath!
*** Warning: in file strassen.v, library seq.v is required and has not been found in loadpath!
*** Warning: in file strassen.v, library choice.v is required and has not been found in loadpath!
*** Warning: in file strassen.v, library fintype.v is required and has not been found in loadpath!
*** Warning: in file strassen.v, library div.v is required and has not been found in loadpath!
*** Warning: in file strassen.v, library finfun.v is required and has not been found in loadpath!
*** Warning: in file strassen.v, library bigop.v is required and has not been found in loadpath!
*** Warning: in file strassen.v, library prime.v is required and has not been found in loadpath!
*** Warning: in file strassen.v, library binomial.v is required and has not been found in loadpath!
*** Warning: in file strassen.v, library ssralg.v is required and has not been found in loadpath!
*** Warning: in file strassen.v, library finset.v is required and has not been found in loadpath!
*** Warning: in file strassen.v, library fingroup.v is required and has not been found in loadpath!
*** Warning: in file strassen.v, library finalg.v is required and has not been found in loadpath!
*** Warning: in file strassen.v, library perm.v is required and has not been found in loadpath!
*** Warning: in file strassen.v, library zmodp.v is required and has not been found in loadpath!
*** Warning: in file strassen.v, library matrix.v is required and has not been found in loadpath!
/usr/bin/coqdep -c -slash -I . "karatsuba.v" > "karatsuba.v.d" || ( RV=$?; rm -f "karatsuba.v.d"; exit ${RV} )
*** Warning: in file karatsuba.v, library ssreflect.v is required and has not been found in loadpath!
*** Warning: in file karatsuba.v, library ssrfun.v is required and has not been found in loadpath!
*** Warning: in file karatsuba.v, library ssrbool.v is required and has not been found in loadpath!
*** Warning: in file karatsuba.v, library eqtype.v is required and has not been found in loadpath!
*** Warning: in file karatsuba.v, library ssrnat.v is required and has not been found in loadpath!
*** Warning: in file karatsuba.v, library div.v is required and has not been found in loadpath!
*** Warning: in file karatsuba.v, library seq.v is required and has not been found in loadpath!
*** Warning: in file karatsuba.v, library path.v is required and has not been found in loadpath!
*** Warning: in file karatsuba.v, library choice.v is required and has not been found in loadpath!
*** Warning: in file karatsuba.v, library fintype.v is required and has not been found in loadpath!
*** Warning: in file karatsuba.v, library tuple.v is required and has not been found in loadpath!
*** Warning: in file karatsuba.v, library finset.v is required and has not been found in loadpath!
*** Warning: in file karatsuba.v, library ssralg.v is required and has not been found in loadpath!
*** Warning: in file karatsuba.v, library poly.v is required and has not been found in loadpath!
*** Warning: in file karatsuba.v, library bigop.v is required and has not been found in loadpath!
/usr/bin/coqdep -c -slash -I . "cseqpolydvd.v" > "cseqpolydvd.v.d" || ( RV=$?; rm -f "cseqpolydvd.v.d"; exit ${RV} )
*** Warning: in file cseqpolydvd.v, library ssreflect.v is required and has not been found in loadpath!
*** Warning: in file cseqpolydvd.v, library ssrfun.v is required and has not been found in loadpath!
*** Warning: in file cseqpolydvd.v, library ssrbool.v is required and has not been found in loadpath!
*** Warning: in file cseqpolydvd.v, library eqtype.v is required and has not been found in loadpath!
*** Warning: in file cseqpolydvd.v, library ssrnat.v is required and has not been found in loadpath!
*** Warning: in file cseqpolydvd.v, library div.v is required and has not been found in loadpath!
*** Warning: in file cseqpolydvd.v, library seq.v is required and has not been found in loadpath!
*** Warning: in file cseqpolydvd.v, library path.v is required and has not been found in loadpath!
*** Warning: in file cseqpolydvd.v, library choice.v is required and has not been found in loadpath!
*** Warning: in file cseqpolydvd.v, library fintype.v is required and has not been found in loadpath!
*** Warning: in file cseqpolydvd.v, library tuple.v is required and has not been found in loadpath!
*** Warning: in file cseqpolydvd.v, library finset.v is required and has not been found in loadpath!
*** Warning: in file cseqpolydvd.v, library ssralg.v is required and has not been found in loadpath!
*** Warning: in file cseqpolydvd.v, library poly.v is required and has not been found in loadpath!
/usr/bin/coqdep -c -slash -I . "cseqpoly.v" > "cseqpoly.v.d" || ( RV=$?; rm -f "cseqpoly.v.d"; exit ${RV} )
*** Warning: in file cseqpoly.v, library ssreflect.v is required and has not been found in loadpath!
*** Warning: in file cseqpoly.v, library ssrfun.v is required and has not been found in loadpath!
*** Warning: in file cseqpoly.v, library ssrbool.v is required and has not been found in loadpath!
*** Warning: in file cseqpoly.v, library eqtype.v is required and has not been found in loadpath!
*** Warning: in file cseqpoly.v, library ssrnat.v is required and has not been found in loadpath!
*** Warning: in file cseqpoly.v, library div.v is required and has not been found in loadpath!
*** Warning: in file cseqpoly.v, library seq.v is required and has not been found in loadpath!
*** Warning: in file cseqpoly.v, library path.v is required and has not been found in loadpath!
*** Warning: in file cseqpoly.v, library choice.v is required and has not been found in loadpath!
*** Warning: in file cseqpoly.v, library fintype.v is required and has not been found in loadpath!
*** Warning: in file cseqpoly.v, library tuple.v is required and has not been found in loadpath!
*** Warning: in file cseqpoly.v, library finset.v is required and has not been found in loadpath!
*** Warning: in file cseqpoly.v, library ssralg.v is required and has not been found in loadpath!
*** Warning: in file cseqpoly.v, library poly.v is required and has not been found in loadpath!
*** Warning: in file cseqpoly.v, library polydiv.v is required and has not been found in loadpath!
/usr/bin/coqdep -c -slash -I . "polydvd.v" > "polydvd.v.d" || ( RV=$?; rm -f "polydvd.v.d"; exit ${RV} )
*** Warning: in file polydvd.v, library ssreflect.v is required and has not been found in loadpath!
*** Warning: in file polydvd.v, library ssrfun.v is required and has not been found in loadpath!
*** Warning: in file polydvd.v, library ssrbool.v is required and has not been found in loadpath!
*** Warning: in file polydvd.v, library eqtype.v is required and has not been found in loadpath!
*** Warning: in file polydvd.v, library ssrnat.v is required and has not been found in loadpath!
*** Warning: in file polydvd.v, library div.v is required and has not been found in loadpath!
*** Warning: in file polydvd.v, library seq.v is required and has not been found in loadpath!
*** Warning: in file polydvd.v, library path.v is required and has not been found in loadpath!
*** Warning: in file polydvd.v, library choice.v is required and has not been found in loadpath!
*** Warning: in file polydvd.v, library fintype.v is required and has not been found in loadpath!
*** Warning: in file polydvd.v, library tuple.v is required and has not been found in loadpath!
*** Warning: in file polydvd.v, library finset.v is required and has not been found in loadpath!
*** Warning: in file polydvd.v, library ssralg.v is required and has not been found in loadpath!
*** Warning: in file polydvd.v, library matrix.v is required and has not been found in loadpath!
*** Warning: in file polydvd.v, library poly.v is required and has not been found in loadpath!
*** Warning: in file polydvd.v, library bigop.v is required and has not been found in loadpath!
*** Warning: in file polydvd.v, library polydiv.v is required and has not been found in loadpath!
/usr/bin/coqdep -c -slash -I . "rank.v" > "rank.v.d" || ( RV=$?; rm -f "rank.v.d"; exit ${RV} )
*** Warning: in file rank.v, library ssreflect.v is required and has not been found in loadpath!
*** Warning: in file rank.v, library ssrfun.v is required and has not been found in loadpath!
*** Warning: in file rank.v, library ssrbool.v is required and has not been found in loadpath!
*** Warning: in file rank.v, library eqtype.v is required and has not been found in loadpath!
*** Warning: in file rank.v, library ssrnat.v is required and has not been found in loadpath!
*** Warning: in file rank.v, library div.v is required and has not been found in loadpath!
*** Warning: in file rank.v, library seq.v is required and has not been found in loadpath!
*** Warning: in file rank.v, library ssralg.v is required and has not been found in loadpath!
*** Warning: in file rank.v, library fintype.v is required and has not been found in loadpath!
*** Warning: in file rank.v, library perm.v is required and has not been found in loadpath!
*** Warning: in file rank.v, library matrix.v is required and has not been found in loadpath!
*** Warning: in file rank.v, library bigop.v is required and has not been found in loadpath!
*** Warning: in file rank.v, library zmodp.v is required and has not been found in loadpath!
*** Warning: in file rank.v, library mxalgebra.v is required and has not been found in loadpath!
/usr/bin/coqdep -c -slash -I . "seqmatrix.v" > "seqmatrix.v.d" || ( RV=$?; rm -f "seqmatrix.v.d"; exit ${RV} )
*** Warning: in file seqmatrix.v, library ssreflect.v is required and has not been found in loadpath!
*** Warning: in file seqmatrix.v, library ssrbool.v is required and has not been found in loadpath!
*** Warning: in file seqmatrix.v, library ssrfun.v is required and has not been found in loadpath!
*** Warning: in file seqmatrix.v, library eqtype.v is required and has not been found in loadpath!
*** Warning: in file seqmatrix.v, library ssrnat.v is required and has not been found in loadpath!
*** Warning: in file seqmatrix.v, library seq.v is required and has not been found in loadpath!
*** Warning: in file seqmatrix.v, library choice.v is required and has not been found in loadpath!
*** Warning: in file seqmatrix.v, library fintype.v is required and has not been found in loadpath!
*** Warning: in file seqmatrix.v, library div.v is required and has not been found in loadpath!
*** Warning: in file seqmatrix.v, library finfun.v is required and has not been found in loadpath!
*** Warning: in file seqmatrix.v, library bigop.v is required and has not been found in loadpath!
*** Warning: in file seqmatrix.v, library prime.v is required and has not been found in loadpath!
*** Warning: in file seqmatrix.v, library binomial.v is required and has not been found in loadpath!
*** Warning: in file seqmatrix.v, library ssralg.v is required and has not been found in loadpath!
*** Warning: in file seqmatrix.v, library finset.v is required and has not been found in loadpath!
*** Warning: in file seqmatrix.v, library fingroup.v is required and has not been found in loadpath!
*** Warning: in file seqmatrix.v, library finalg.v is required and has not been found in loadpath!
*** Warning: in file seqmatrix.v, library perm.v is required and has not been found in loadpath!
*** Warning: in file seqmatrix.v, library zmodp.v is required and has not been found in loadpath!
*** Warning: in file seqmatrix.v, library matrix.v is required and has not been found in loadpath!
/usr/bin/coqdep -c -slash -I . "Qinfra.v" > "Qinfra.v.d" || ( RV=$?; rm -f "Qinfra.v.d"; exit ${RV} )
*** Warning: in file Qinfra.v, library ssreflect.v is required and has not been found in loadpath!
*** Warning: in file Qinfra.v, library ssrbool.v is required and has not been found in loadpath!
*** Warning: in file Qinfra.v, library eqtype.v is required and has not been found in loadpath!
*** Warning: in file Qinfra.v, library ssrnat.v is required and has not been found in loadpath!
*** Warning: in file Qinfra.v, library seq.v is required and has not been found in loadpath!
*** Warning: in file Qinfra.v, library choice.v is required and has not been found in loadpath!
*** Warning: in file Qinfra.v, library fintype.v is required and has not been found in loadpath!
*** Warning: in file Qinfra.v, library finfun.v is required and has not been found in loadpath!
*** Warning: in file Qinfra.v, library ssrfun.v is required and has not been found in loadpath!
*** Warning: in file Qinfra.v, library bigop.v is required and has not been found in loadpath!
*** Warning: in file Qinfra.v, library ssralg.v is required and has not been found in loadpath!
/usr/bin/coqdep -c -slash -I . "Zinfra.v" > "Zinfra.v.d" || ( RV=$?; rm -f "Zinfra.v.d"; exit ${RV} )
*** Warning: in file Zinfra.v, library ssreflect.v is required and has not been found in loadpath!
*** Warning: in file Zinfra.v, library ssrfun.v is required and has not been found in loadpath!
*** Warning: in file Zinfra.v, library ssrbool.v is required and has not been found in loadpath!
*** Warning: in file Zinfra.v, library eqtype.v is required and has not been found in loadpath!
*** Warning: in file Zinfra.v, library ssrnat.v is required and has not been found in loadpath!
*** Warning: in file Zinfra.v, library div.v is required and has not been found in loadpath!
*** Warning: in file Zinfra.v, library ssralg.v is required and has not been found in loadpath!
*** Warning: in file Zinfra.v, library seq.v is required and has not been found in loadpath!
*** Warning: in file Zinfra.v, library choice.v is required and has not been found in loadpath!
*** Warning: in file Zinfra.v, library fintype.v is required and has not been found in loadpath!
*** Warning: in file Zinfra.v, library finfun.v is required and has not been found in loadpath!
*** Warning: in file Zinfra.v, library bigop.v is required and has not been found in loadpath!
/usr/bin/coqdep -c -slash -I . "cdvdring.v" > "cdvdring.v.d" || ( RV=$?; rm -f "cdvdring.v.d"; exit ${RV} )
*** Warning: in file cdvdring.v, library ssreflect.v is required and has not been found in loadpath!
*** Warning: in file cdvdring.v, library ssrfun.v is required and has not been found in loadpath!
*** Warning: in file cdvdring.v, library ssrbool.v is required and has not been found in loadpath!
*** Warning: in file cdvdring.v, library eqtype.v is required and has not been found in loadpath!
*** Warning: in file cdvdring.v, library ssrnat.v is required and has not been found in loadpath!
*** Warning: in file cdvdring.v, library div.v is required and has not been found in loadpath!
*** Warning: in file cdvdring.v, library seq.v is required and has not been found in loadpath!
*** Warning: in file cdvdring.v, library path.v is required and has not been found in loadpath!
*** Warning: in file cdvdring.v, library ssralg.v is required and has not been found in loadpath!
*** Warning: in file cdvdring.v, library fintype.v is required and has not been found in loadpath!
*** Warning: in file cdvdring.v, library perm.v is required and has not been found in loadpath!
*** Warning: in file cdvdring.v, library tuple.v is required and has not been found in loadpath!
*** Warning: in file cdvdring.v, library choice.v is required and has not been found in loadpath!
*** Warning: in file cdvdring.v, library matrix.v is required and has not been found in loadpath!
*** Warning: in file cdvdring.v, library bigop.v is required and has not been found in loadpath!
*** Warning: in file cdvdring.v, library zmodp.v is required and has not been found in loadpath!
*** Warning: in file cdvdring.v, library mxalgebra.v is required and has not been found in loadpath!
*** Warning: in file cdvdring.v, library poly.v is required and has not been found in loadpath!
/usr/bin/coqdep -c -slash -I . "dvdring.v" > "dvdring.v.d" || ( RV=$?; rm -f "dvdring.v.d"; exit ${RV} )
*** Warning: in file dvdring.v, library ssreflect.v is required and has not been found in loadpath!
*** Warning: in file dvdring.v, library ssrfun.v is required and has not been found in loadpath!
*** Warning: in file dvdring.v, library ssrbool.v is required and has not been found in loadpath!
*** Warning: in file dvdring.v, library eqtype.v is required and has not been found in loadpath!
*** Warning: in file dvdring.v, library ssrnat.v is required and has not been found in loadpath!
*** Warning: in file dvdring.v, library div.v is required and has not been found in loadpath!
*** Warning: in file dvdring.v, library seq.v is required and has not been found in loadpath!
*** Warning: in file dvdring.v, library path.v is required and has not been found in loadpath!
*** Warning: in file dvdring.v, library ssralg.v is required and has not been found in loadpath!
*** Warning: in file dvdring.v, library fintype.v is required and has not been found in loadpath!
*** Warning: in file dvdring.v, library perm.v is required and has not been found in loadpath!
*** Warning: in file dvdring.v, library tuple.v is required and has not been found in loadpath!
*** Warning: in file dvdring.v, library choice.v is required and has not been found in loadpath!
*** Warning: in file dvdring.v, library matrix.v is required and has not been found in loadpath!
*** Warning: in file dvdring.v, library bigop.v is required and has not been found in loadpath!
*** Warning: in file dvdring.v, library zmodp.v is required and has not been found in loadpath!
*** Warning: in file dvdring.v, library mxalgebra.v is required and has not been found in loadpath!
*** Warning: in file dvdring.v, library poly.v is required and has not been found in loadpath!
*** Warning: in file dvdring.v, library generic_quotient.v is required and has not been found in loadpath!
/usr/bin/coqdep -c -slash -I . "cssralg.v" > "cssralg.v.d" || ( RV=$?; rm -f "cssralg.v.d"; exit ${RV} )
*** Warning: in file cssralg.v, library ssreflect.v is required and has not been found in loadpath!
*** Warning: in file cssralg.v, library ssrfun.v is required and has not been found in loadpath!
*** Warning: in file cssralg.v, library ssrbool.v is required and has not been found in loadpath!
*** Warning: in file cssralg.v, library eqtype.v is required and has not been found in loadpath!
*** Warning: in file cssralg.v, library ssrnat.v is required and has not been found in loadpath!
*** Warning: in file cssralg.v, library div.v is required and has not been found in loadpath!
*** Warning: in file cssralg.v, library seq.v is required and has not been found in loadpath!
*** Warning: in file cssralg.v, library path.v is required and has not been found in loadpath!
*** Warning: in file cssralg.v, library fintype.v is required and has not been found in loadpath!
*** Warning: in file cssralg.v, library tuple.v is required and has not been found in loadpath!
*** Warning: in file cssralg.v, library finset.v is required and has not been found in loadpath!
*** Warning: in file cssralg.v, library ssralg.v is required and has not been found in loadpath!
*** Warning: in file cssralg.v, library bigop.v is required and has not been found in loadpath!
/usr/bin/coqdep -c -slash -I . "ssrcomplements.v" > "ssrcomplements.v.d" || ( RV=$?; rm -f "ssrcomplements.v.d"; exit ${RV} )
*** Warning: in file ssrcomplements.v, library ssreflect.v is required and has not been found in loadpath!
*** Warning: in file ssrcomplements.v, library ssrfun.v is required and has not been found in loadpath!
*** Warning: in file ssrcomplements.v, library ssrbool.v is required and has not been found in loadpath!
*** Warning: in file ssrcomplements.v, library eqtype.v is required and has not been found in loadpath!
*** Warning: in file ssrcomplements.v, library ssrnat.v is required and has not been found in loadpath!
*** Warning: in file ssrcomplements.v, library div.v is required and has not been found in loadpath!
*** Warning: in file ssrcomplements.v, library seq.v is required and has not been found in loadpath!
*** Warning: in file ssrcomplements.v, library path.v is required and has not been found in loadpath!
*** Warning: in file ssrcomplements.v, library ssralg.v is required and has not been found in loadpath!
*** Warning: in file ssrcomplements.v, library fintype.v is required and has not been found in loadpath!
*** Warning: in file ssrcomplements.v, library finfun.v is required and has not been found in loadpath!
*** Warning: in file ssrcomplements.v, library perm.v is required and has not been found in loadpath!
*** Warning: in file ssrcomplements.v, library matrix.v is required and has not been found in loadpath!
*** Warning: in file ssrcomplements.v, library bigop.v is required and has not been found in loadpath!
*** Warning: in file ssrcomplements.v, library zmodp.v is required and has not been found in loadpath!
*** Warning: in file ssrcomplements.v, library mxalgebra.v is required and has not been found in loadpath!
*** Warning: in file ssrcomplements.v, library choice.v is required and has not been found in loadpath!
*** Warning: in file ssrcomplements.v, library poly.v is required and has not been found in loadpath!
*** Warning: in file ssrcomplements.v, library polydiv.v is required and has not been found in loadpath!
*** Warning: in file ssrcomplements.v, library mxpoly.v is required and has not been found in loadpath!
*** Warning: in file ssrcomplements.v, library binomial.v is required and has not been found in loadpath!
make[1]: Leaving directory /home/martin/geo/CoqEAL/v0.1' make[1]: ocamlc.opt: Command not found make[1]: Entering directory/home/martin/geo/CoqEAL/v0.1'
make[1]: Nothing to be done for Makefile'. make[1]: Leaving directory/home/martin/geo/CoqEAL/v0.1'
/bin/mkdir -p bin
make -f Makefile.coq all
make[1]: ocamlc.opt: Command not found
make[1]: Entering directory /home/martin/geo/CoqEAL/v0.1' /usr/bin/coqc -q -I . ssrcomplements File "./ssrcomplements.v", line 3, characters 0-67: Error: Cannot find library ssreflect in loadpath make[1]: *** [ssrcomplements.vo] Error 1 make[1]: Leaving directory/home/martin/geo/CoqEAL/v0.1'
make: *** [all] Error 2
martin@ubuntu:/geo/CoqEAL/v0.1$ export COQBIN=/usr/bin/
martin@ubuntu:/geo/CoqEAL/v0.1$ export SSRSRC=/home/martin/geo/CoqEAL/theory/
martin@ubuntu:/geo/CoqEAL/v0.1$ export SSRLIB=/home/martin/geo/CoqEAL/
martin@ubuntu:/geo/CoqEAL/v0.1$ make
make -f Makefile.coq Makefile
make[1]: ocamlc.opt: Command not found
make[1]: Entering directory /home/martin/geo/CoqEAL/v0.1' make[1]: Nothing to be done forMakefile'.
make[1]: Leaving directory /home/martin/geo/CoqEAL/v0.1' /bin/mkdir -p bin make -f Makefile.coq all make[1]: ocamlc.opt: Command not found make[1]: Entering directory/home/martin/geo/CoqEAL/v0.1'
/usr/bin/coqc -q -I . ssrcomplements
File "./ssrcomplements.v", line 3, characters 0-67:
Error: Cannot find library ssreflect in loadpath
make[1]: *** [ssrcomplements.vo] Error 1
make[1]: Leaving directory `/home/martin/geo/CoqEAL/v0.1'
make: *** [all] Error 2
martin@ubuntu:~/geo/CoqEAL/v0.1$

martin@ubuntu:/geo/CoqEAL/theory$ which coq
martin@ubuntu:/geo/CoqEAL/theory$
martin@ubuntu:~/geo/CoqEAL$ pwd
/home/martin/geo/CoqEAL

martin@ubuntu:~/geo/CoqEAL/v0.1$ coqc -v
The Coq Proof Assistant, version 8.3pl4 (April 2012)
compiled on Apr 03 2012 10:32:56 with OCaml 3.12.1

export COQBIN=/usr/bin/coqc
export SSRSRC=/home/martin/geo/CoqEAL/theory
export SSRLIB=/home/martin/geo/CoqEAL

martin@ubuntu:~/geo/CoqEAL/v0.1$ make
/usr/bin/coqccoq_makefile -f Make -o Makefile.coq
make: /usr/bin/coqccoq_makefile: Command not found
make: *** [Makefile.coq] Error 127

martin@ubuntu:~/geo/CoqEAL/theory$ lsb_release -a
No LSB modules are available.
Distributor ID: Ubuntu
Description: Ubuntu 12.04.4 LTS
Release: 12.04
Codename: precise

In order to compile this library, you have to set three environment variables:

• COQBIN should be the path to Coq's binaries (coqc, coqdep,...)
• SSRSRC should be the path to the ssreflect "src" folder
  (in which ssreflect.cmxs can be found).
• SSRLIB should be the path to ssr theories (where the .vo files are)

To set environment variables, you may use a command like:
export SSRSRC=/path/...

and then type make to compile

There seems to be a checksum problem with coqeal 1.0.5

% opam install coq-coqeal
The following actions will be performed:
  - install coq-mathcomp-multinomials 1.5.4         [required by coq-coqeal]
  - install coq-paramcoq              1.1.2+coq8.13 [required by coq-coqeal]
  - install coq-coqeal                1.0.5
===== 3 to install =====
Do you want to continue? [Y/n] y

<><> Gathering sources ><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
[coq-paramcoq.1.1.2+coq8.13] downloaded from https://github.com/coq-community/paramcoq/archive/v1.1.2+coq8.13.tar.gz
[coq-mathcomp-multinomials.1.5.4] downloaded from https://github.com/math-comp/multinomials/archive/1.5.4.tar.gz
[ERROR] The sources of the following couldn't be obtained, aborting:
          - coq-coqeal.1.0.5: Bad checksum

I'm updating the mathcomp packages in Debian, and with mathcomp 1.15.0, I get issues with coqeal:

File "./refinements/binrat.v", line 314, characters 34-45:
Error:
In environment
n : BinNums.Z
The term "(1%Z, (n, 1%Z))" has type "(int * (BinNums.Z * int))%type"
while it is expected to have type
 "(BinNums.Z * (BinNums.Z * BinNums.Z))%type".

make[3]: *** [Makefile.coq:763: refinements/binrat.vo] Error 1
make[3]: *** Waiting for unfinished jobs....
File "./refinements/seqpoly.v", line 733, characters 47-48:
Error:
The term "3" has type "GRing.Zmodule.sort ?t"
while it is expected to have type "Equality.sort nat_eqType".

make[3]: *** [Makefile.coq:763: refinements/seqpoly.vo] Error 1
File "./refinements/hpoly.v", line 903, characters 46-47:
Error:
The term "3" has type "GRing.Zmodule.sort ?t"
while it is expected to have type "nat".

I suspect you have already fixed those in git, but there's no official release yet : can you tag one, please? Thanks!

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 the opam package we are currently testing in Coq Platform CI works fine with Coq 8.15.0.

Coq Platform CI is currently testing opam package coq-coqeal.1.1.0
from official repository https://coq.inria.fr/opam/released/packages/coq-coqeal/coq-coqeal.1.1.0/opam.

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 2022.02, please inform us as soon as possible and before February 14, 2022!

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.

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#193

I have trouble compiling CoqEAL with Coq 8.10.1 and Mathematical Components 1.9. And more precisely I have trouble finding the right dependencies:

• I had to add a no-template-check option to coqtop in the Makfile in order to compile refinements/param.v This seems consistent with the current test-suite of coq-param, but is a bit unfortunate isn't it? @proux01 is it the right thing to do?

• multinomials is in the dependencies, which itself depend on finmap. But finmap does not seem to tag a specific version for Coq 8.10.1+ MathComp 1.9 So I tried 1.3.4. But then multinomials does not compile.

Is there a way to get all this to work (possibly at the price of the no-template-check option)? If so could you document it and tag the right versions in the corresponding repos, including this one?

After #54 is merged, we need to consolidate some material and possibly reorganize it a bit. I open this issue as a memento.

So far, we have at least the following mentioned by Cyril:

the companion matrix has been added to mathcomp already.

Thanks to porting effort by @ybertot, the matrix normal/canonical forms by Guillaume Cano have been ported to recent Coq and MathComp, and relies on the latest CoqEAL.

However, at around 2,200 lines of code, this is a small library that is not likely to get a lot of maintenance effort. If we instead consolidate the library into CoqEAL, we may be able to conserve resources and provide the results to a wider audience (since CoqEAL is planned to be part of the Coq platform).

What are the tradeoffs?

• The code depends on MathComp real-closed, which is not currently a dependency of CoqEAL. This will add to time to build in CI. On the other hand, real-closed is also planned to be included in the Coq platform.
• The code depends directly on MathComp fingroup, which is nevertheless a dependency of MathComp algebra which CoqEAL already depends on.
• More code to maintain in CoqEAL.

What do you think @proux01 and @ybertot?

This is obviously not a high priority issue, but if you give the go-ahead, I can set up the transfer in the near future. Essentially, we would just archive the matrix canonical forms repo for posterity with a pointer to CoqEAL.