Sergei Meshveliani (Jun 30 2021 at 17:43): 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
Enrico Tassi (Jun 30 2021 at 17:59):CC @Cyril Cohen
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?
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.
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)
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:
Cyril Cohen (Jul 01 2021 at 10:14):(I picked a random lemma added in 1.12.0 from the changelog
[technical explication]
)
Gaëtan Gilbert (Jul 01 2021 at 10:17):/snap is suspicious
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.
?
Gaëtan Gilbert (Jul 01 2021 at 10:25):you forgot the ending .
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.)
?
Enrico Tassi (Jul 01 2021 at 10:38):Where did you read all? maybe all_ssreflect or all_algebra?
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.
Enrico Tassi (Jul 01 2021 at 10:39):(but you don't have coqEAL available)
Cyril Cohen (Jul 01 2021 at 10:42):Cyril Cohen said:
ok... can you type this:
coqtopand 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.
> ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
...
Coq <
Is it ready to work with MatcComp ?
Cyril Cohen (Jul 01 2021 at 11:00):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 ?
Cyril Cohen (Jul 01 2021 at 11:04):yes, let's go there
Sergei Meshveliani (Jul 01 2021 at 11:07):Has it sense to install CoqEAL from source by make, make install ?
Cyril Cohen (Jul 01 2021 at 11:11):Yes, provided all the dependencies are installed. You should also check that paramcoq is installed.
Pierre Roux (Jul 01 2021 at 11:17):You'll also need bignums and multinomials https://github.com/CoqEAL/CoqEAL#meta
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
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 ?
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)
Sergei Meshveliani (Jul 01 2021 at 12:10):I see. Thanks to people.
I am going to do everything by new with opam.
Cyril Cohen (Jul 01 2021 at 12:11):Good luck, it should be easier to install the required libraries after that
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
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?
Cyril Cohen (Jul 01 2021 at 17:50):Now, do you want to contribute to CoqEAL or use it?
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?
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 ?)
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: Sep 25 2023 at 14:01 UTC