Stream: Coq users

Topic: installing CoqEAL


view this post on Zulip Sergei Meshveliani (Jun 30 2021 at 17:43):

People,
I have installed Coq 8.13.2 (on Ubuntu Linux 18.04). Then I needed the MathComp library.
But it occurs that it is already in Coq 8.13.2.
Then I need to install CoqEAL (Effective Algebra library)
on top of all this.
And have difficulties with installing it from source via `make'.
But may be it is already in this Coq, similarly as MathComp ?

Thanks,


Sergei

view this post on Zulip Enrico Tassi (Jun 30 2021 at 17:59):

CC @Cyril Cohen

view this post on Zulip Cyril Cohen (Jun 30 2021 at 18:00):

Sergei said:

People,
I have installed Coq 8.13.2 (on Ubuntu Linux 18.04). Then I needed the MathComp library.
But it occurs that it is already in Coq 8.13.2.
Then I need to install CoqEAL (Effective Algebra library)
on top of all this.
And have difficulties with installing it from source via `make'.
But may be it is already in this Coq, similarly as MathComp ?

Thanks,


Sergei

Hi Sergei, can you please tell me how you installed Coq and mathcomp?

view this post on Zulip Sergei Meshveliani (Jul 01 2021 at 10:06):

Coq has been installed from the package for Linux,
I recall, probably, by
$ sudo apt update
$ sudo apt install coq

$ coqc -v
The Coq Proof Assistant, version 8.13.2 (April 2021) compiled on Apr 9 2021 11:34:01 with OCaml 4.07.1

$ which coqc
/snap/bin/coqc

Then I tried to install MathComp from source by "make" . But after the the "build" phase,
it failed to overwrite many files in the system area, I recall, in /snap/...
People wrote me that this is probably because MathComp has been installed automatically together with Coq 8.13.2.
And I have the same impression, due to the file paths mentioned in the message of 'make'.
So, I believe now that MathComp is already installed (how to test this?)
and it remains to install CoqEAL.
?
My aim is to run certain existing programs under CoqEAL.
But so far I never tried anything are all with Coq, except coqc -v.

view this post on Zulip Cyril Cohen (Jul 01 2021 at 10:12):

ok... can you type this:

coqtop

and then, when prompted

From mathcomp Require Import all_ssreflect all_algebra all_field.

(fixed)

view this post on Zulip Cyril Cohen (Jul 01 2021 at 10:13):

If this work you have some version of mathcomp installed, to know which one we do not have a canonical way, but you can type

Check take_uniq.

If this command succeeds, it means you have mathcomp >= 1.12 :joy:

view this post on Zulip Cyril Cohen (Jul 01 2021 at 10:14):

(I picked a random lemma added in 1.12.0 from the changelog

[technical explication]

)

view this post on Zulip Gaëtan Gilbert (Jul 01 2021 at 10:17):

/snap is suspicious

view this post on Zulip Sergei Meshveliani (Jul 01 2021 at 10:23):

This goes as follows

$ coqtop
Welcome to Coq 8.13.2 (April 2021)

>  rom mathcomp Require Import all.
Error: Syntax error: illegal begin of toplevel:vernac_toplevel.

Coq <  From mathcomp Require Import all
Coq <  Check take_uniq
Coq <

I recall: several days ago I looked into the MathComp book, and tried to enter various simple commands taken from this book. And the result printing was always as above - the empty line.
?

view this post on Zulip Gaëtan Gilbert (Jul 01 2021 at 10:25):

you forgot the ending .

view this post on Zulip Sergei Meshveliani (Jul 01 2021 at 10:35):

I thought this period is not a part of the syntax!
Now, start by new:

Welcome to Coq 8.13.2 (April 2021)

Coq < From mathcomp Require Import all.
Toplevel input, characters 29-32:
Coq > From mathcomp Require Import all.
>                                                                              ^^^
Error: Unable to locate library
all with prefix mathcomp. (While searching for a .vos file.)

?

view this post on Zulip Enrico Tassi (Jul 01 2021 at 10:38):

Where did you read all? maybe all_ssreflect or all_algebra?

view this post on Zulip Enrico Tassi (Jul 01 2021 at 10:38):

About the mathcomp book, you can play the snippets in your browser: https://math-comp.github.io/mcb/ with no installation required.

view this post on Zulip Enrico Tassi (Jul 01 2021 at 10:39):

(but you don't have coqEAL available)

view this post on Zulip Cyril Cohen (Jul 01 2021 at 10:42):

Cyril Cohen said:

ok... can you type this:

coqtop

and then, when prompted

From mathcomp Require Import all.

Oh, all may not be installed by opam/ubuntu :laughing:
@Sergei my bad, try the following:

coqtop

and then, when prompted

From mathcomp Require Import all_ssreflect all_algebra all_field.

view this post on Zulip Sergei Meshveliani (Jul 01 2021 at 10:48):

I see. Now I try

Coq> From mathcomp Require Import all_ssreflect all_algebra all_field.
...
Warning:
New coercion path [GRing.subalg_closedBM; GRing.subring_closedB] : GRing.subalg_closed >-> GRing.zmod_closed is ambiguous with existing
[GRing.subalg_closedZ; GRing.submod_closedB] : GRing.subalg_closed >-> GRing.zmod_closed.
[ambiguous-paths,typechecker]
Toplevel input, characters 0-65:
> From mathcomp Require Import all_ssreflect all_algebra all_field.
> ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
...
Coq <

Is it ready to work with MatcComp ?

view this post on Zulip Cyril Cohen (Jul 01 2021 at 11:00):

Yes, now please type:

Check take_uniq.

view this post on Zulip Sergei Meshveliani (Jul 01 2021 at 11:03):

Coq < Check take_uniq.
take_uniq
     : forall (T : eqType) (s : seq T) (n : nat), uniq s -> uniq (take n s)

Coq <

It look like it works.
Now, install CoqEAL ?

view this post on Zulip Cyril Cohen (Jul 01 2021 at 11:04):

yes, let's go there

view this post on Zulip Sergei Meshveliani (Jul 01 2021 at 11:07):

Has it sense to install CoqEAL from source by make, make install ?

view this post on Zulip Cyril Cohen (Jul 01 2021 at 11:11):

Yes, provided all the dependencies are installed. You should also check that paramcoq is installed.

view this post on Zulip Pierre Roux (Jul 01 2021 at 11:17):

You'll also need bignums and multinomials https://github.com/CoqEAL/CoqEAL#meta

view this post on Zulip Cyril Cohen (Jul 01 2021 at 11:39):

In the end you are probably better off by uninstalling your systemwide coq and installing everything via opam

view this post on Zulip Sergei Meshveliani (Jul 01 2021 at 11:58):

I have the directory CoqEAL-1.0.5/ with the CoqEAL-1.0.5 source,
and have opam-1.2.2 installed hour ago. Following README.md of CoqEAL,
I command

> opam repo add coq-released https://coq.inria.fr/opam/released

It reports

# opam-version    1.2.2
# os              linux
File /home/mechvel/.opam/config does not exist

I wonder: where the .opam/config could reside?
I have installed opam by apt install opam, and now I see the file /usr/bin/opam.
I do not know any about opam.
Need I to create manually an empty file /home/mechvel/.opam/config ?

view this post on Zulip Cyril Cohen (Jul 01 2021 at 12:06):

You need to follow the full instructions at https://coq.inria.fr/opam-using.html first (including the initialization step that you apparently miss)

view this post on Zulip Sergei Meshveliani (Jul 01 2021 at 12:10):

I see. Thanks to people.
I am going to do everything by new with opam.

view this post on Zulip Cyril Cohen (Jul 01 2021 at 12:11):

Good luck, it should be easier to install the required libraries after that

view this post on Zulip Théo Zimmermann (Jul 01 2021 at 12:53):

Note that the easiest way to install via opam is to use the interactive platform installer. It will also already include a number of dependencies of CoqEAL, if not all: https://github.com/coq/platform/blob/2021.02/README_Linux.md#installation-by-compiling-from-sources-using-opam

view this post on Zulip Sergei Meshveliani (Jul 01 2021 at 17:45):

Now, I have installed opam-2.1.0~rc2
(which was said "a stable version", but the suffix "rc2" looks as of a candidate version).
Than I have installed Coq 8.13.2 by using opam, following the instruction of installing Coq
on coq.inria.fr....
Then:

> which coqtop
/home/mechvel/.opam/default/bin/coqtop

> coqtop
Welcome to Coq 8.13.2 (July 2021)

Coq < From mathcomp Require Import all_ssreflect all_algebra all_field.
Toplevel input, characters 29-42:
> From mathcomp Require Import all_ssreflect all_algebra all_field.
>                              ^^^^^^^^^^^^^
Error: Cannot find a physical path bound to logical path matching suffix
<> and prefix mathcomp.

Now, is MathComp there?

view this post on Zulip Cyril Cohen (Jul 01 2021 at 17:50):

Now, do you want to contribute to CoqEAL or use it?

view this post on Zulip Sergei Meshveliani (Jul 01 2021 at 17:57):

I want only to use MathComp and CoqEAL.

But I suspect that MathComp is not installed this time together with Coq.
Is it?
So, I see https://math-comp.github.io/installation.html, and am trying to install the MathComp parts by following its instruction.
Is this all right?

view this post on Zulip Cyril Cohen (Jul 01 2021 at 18:03):

OK, so you can simply type

opam install coq-coqeal

it will install CoqEAL and its dependencies including a few mathcomp packages, (which ones do you need by the way ?)

view this post on Zulip Sergei Meshveliani (Jul 01 2021 at 18:25):

I looked into PhD thesis by Moertberg (2014), and I want to observe his certified program for the Karatsuba method to multiply univariate polynomials, to have an impression of all the code. And it is written that it is on CoqEAL.
Also I want to see how is there programmed certified arithmetic for univariate polynomials over a CommutativeRing, and to run examples with this arithmetic for the coefficients of Integer and of Integer modulo b (Integer/(b)).
What libraries do I need to join?
But I never tried anything with Coq.
So far, I need to start with simplest things. Say, to program summing of a list of integers and run it.

By using opam, I have installed now coq-mathcomp-ssreflect, coq-mathcomp-algebra, coq-mathcomp-field,
Now, I am trying

 > opam install coq-coqeal

and hope this would not contradict to the previous actions ...


Last updated: Jan 31 2023 at 14:03 UTC