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

CC @Cyril Cohen

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?

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`

.

ok... can you type this:

```
coqtop
```

and then, when prompted

```
From mathcomp Require Import all_ssreflect all_algebra all_field.
```

(fixed)

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:

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

[technical explication]

)

/snap is suspicious

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.

?

you forgot the ending `.`

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.)
```

?

Where did you read `all`

? maybe `all_ssreflect`

or `all_algebra`

?

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

(but you don't have coqEAL available)

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.
```

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.
> ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
...
```

- many warnings of this kind. And it ends with

```
Coq <
```

Is it ready to work with MatcComp ?

Yes, now please type:

```
Check take_uniq.
```

```
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 ?

yes, let's go there

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

?

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

is installed.

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

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

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`

?

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

I see. Thanks to people.

I am going to do everything by new with `opam`

.

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

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

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?

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

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?

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 ?)

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: Sep 25 2023 at 14:01 UTC