Stream: Coq users

Topic: mathcomp on platform


view this post on Zulip Darij Grinberg (Feb 18 2022 at 19:59):

Hi! Absolute newbie question here (my meager skills from 5 ago have rusted). I've just installed the Coq Platform on my Win10. Supposedly it has the mathcomp libs. Where do I find those?

view this post on Zulip Ana de Almeida Borges (Feb 18 2022 at 20:00):

You can import mathcomp stuff with From mathcomp Require Import <name>, for example From mathcomp Require Import all_ssreflect.. Does this work?

view this post on Zulip Darij Grinberg (Feb 18 2022 at 20:01):

ah! but can I find the .v files itself somewhere in the hierarchy?

view this post on Zulip Darij Grinberg (Feb 18 2022 at 20:02):

yeah the imports work

view this post on Zulip Darij Grinberg (Feb 18 2022 at 20:02):

oh in user-contrib

view this post on Zulip Darij Grinberg (Feb 18 2022 at 20:03):

is this where I put my own .vs too?

view this post on Zulip Ana de Almeida Borges (Feb 18 2022 at 20:05):

Uh, I don't think that's advised. Usually I put my .v files wherever I feel like on my computer (eg, in a work/project directory). When you compile from there, you can still import the libraries installed with the Platform. If you then want to use one of your personal projects in another personal project, then you have several options that we can discuss if you want (but I get the impression that is not really what you are asking).

view this post on Zulip Darij Grinberg (Feb 18 2022 at 20:06):

Oh, it is what I wanted to ask a few questions later :) thank you!

view this post on Zulip Darij Grinberg (Feb 18 2022 at 20:07):

to be specific, I want to import files from a project in the same project

view this post on Zulip Darij Grinberg (Feb 18 2022 at 20:07):

i think all its dependencies are in the platform already, but it is not

view this post on Zulip Ana de Almeida Borges (Feb 18 2022 at 20:07):

The fact that the place where mathcomp lives happens to be called user-contrib doesn't mean users should put their projects there, just that mathcomp was developed by "users" who then contributed their development to Coq, and the Coq (or Platform) developers decided to store them in a place called user-contrib. At least that's my understanding.

view this post on Zulip Darij Grinberg (Feb 18 2022 at 20:07):

to complicate things, it has been "transferred to mathcomp", but I don't know what it means

view this post on Zulip Gaëtan Gilbert (Feb 18 2022 at 20:08):

user-contrib is where projects from "users" get installed by coq_makefile make install

view this post on Zulip Ana de Almeida Borges (Feb 18 2022 at 20:08):

What does "transferred to mathcomp" mean? Is this a public project you can link to, or a personal project of yours?

view this post on Zulip Darij Grinberg (Feb 18 2022 at 20:09):

I don't know what it means :) the project is https://github.com/math-comp/Coq-Combi

view this post on Zulip Darij Grinberg (Feb 18 2022 at 20:09):

i'm pretty sure its content is not in the parts of mathcomp that are on the platform

view this post on Zulip Darij Grinberg (Feb 18 2022 at 20:09):

maybe just transferring the github owner

view this post on Zulip Ana de Almeida Borges (Feb 18 2022 at 20:10):

Darij Grinberg said:

maybe just transferring the github owner

Probably that's what it means, yes

view this post on Zulip Ana de Almeida Borges (Feb 18 2022 at 20:11):

Darij Grinberg said:

to be specific, I want to import files from a project in the same project

Are you developing / changing / adding to Coq-Combi, or do you want to use it as-is and write your own files where you import stuff from Coq-Combi?

view this post on Zulip Darij Grinberg (Feb 18 2022 at 20:11):

ideally, both

view this post on Zulip Ana de Almeida Borges (Feb 18 2022 at 20:14):

For the former, I would clone Coq-Combi (or a fork of Coq-Combi) and confirm that all the dependencies are there by trying to compile the project (probably make works). Then you could manipulate the files as needed. (I'm using a lot of jargon - let me know if something is unclear).

view this post on Zulip Darij Grinberg (Feb 18 2022 at 20:15):

Cloned it, but where should I run make from? From WSFL?

view this post on Zulip Ana de Almeida Borges (Feb 18 2022 at 20:16):

From the main directory, the one where the makefile is

view this post on Zulip Darij Grinberg (Feb 18 2022 at 20:17):

from what kind of console?

view this post on Zulip Ana de Almeida Borges (Feb 18 2022 at 20:17):

right, you're using Windows. I actually have no idea, sorry. But you can try any console you can get your hands on?

view this post on Zulip Darij Grinberg (Feb 18 2022 at 20:18):

ah, is the output system-independent?

view this post on Zulip Ana de Almeida Borges (Feb 18 2022 at 20:19):

Uhh, I think it depends on what is in the .v files, but truthfully I don't know anything about this. I just don't know how makefiles and Windows interact. Perhaps everything works fine, perhaps not. I was just trying to convey my ignorance here.

view this post on Zulip Ana de Almeida Borges (Feb 18 2022 at 20:19):

Maybe, if that doesn't work, you can try to compile through CoqIDE, I think there is an option for that.

view this post on Zulip Ana de Almeida Borges (Feb 18 2022 at 20:20):

(assuming you are using CoqIDE)

view this post on Zulip Darij Grinberg (Feb 18 2022 at 20:20):

i've tried CoqIDE; it just gave me "Compilation output:" and i found no new files in the folder

view this post on Zulip Darij Grinberg (Feb 18 2022 at 20:21):

anyway thanks a lot for answering my first few questions!

view this post on Zulip Ana de Almeida Borges (Feb 18 2022 at 20:22):

Ok. You're welcome and I hope someone else can come answer your remaining questions, about which I am really out of my depth.

view this post on Zulip Paolo Giarrusso (Feb 18 2022 at 20:51):

There are hints in https://github.com/coq/platform, but they're a bit hidden (cc @Michael Soegtrop ) under "Features of the Coq Platform"

view this post on Zulip Paolo Giarrusso (Feb 18 2022 at 20:52):

for Windows there is an additional wrapper batch script to setup Cygwin as build and working environment

view this post on Zulip Paolo Giarrusso (Feb 18 2022 at 20:55):

@Darij Grinberg I don’t have Windows but WSL could run the Linux Coq Platform; since you used the Windows installer, you should likely use a Windows prompt

view this post on Zulip Paolo Giarrusso (Feb 18 2022 at 20:56):

or check if the platform comes with tools to set the right build environment

view this post on Zulip Paolo Giarrusso (Feb 18 2022 at 20:59):

oh: https://github.com/coq/platform#installation-of-other-packages says “On Windows open a shell with C:\<your_coq_platform_cygwin_path>\cygwin.bat.

view this post on Zulip Paolo Giarrusso (Feb 18 2022 at 21:01):

from the instructions, I think in that shell you’d be able to cd to the checkout of Coq-Combi, type make, and everything work.

view this post on Zulip Paolo Giarrusso (Feb 18 2022 at 21:02):

my remaining question: do the instructions suggest to double-click on that batch file, or to run it from inside another shell?

view this post on Zulip Darij Grinberg (Feb 18 2022 at 21:04):

oh! can I use cygwin independently of how i installed the coq platform?

view this post on Zulip Darij Grinberg (Feb 18 2022 at 21:04):

or do I need to install the Linux platform under cygwin for that?

view this post on Zulip Darij Grinberg (Feb 18 2022 at 21:05):

I don't think I have a cygwin bat anywhere in my coq platform

view this post on Zulip Darij Grinberg (Feb 18 2022 at 21:05):

and i rather not install it under cygwin, as that would make it hard to get coqide to run

view this post on Zulip Darij Grinberg (Feb 18 2022 at 21:06):

i'm fine with manually compiling the files one after the other on coqide, but coqide doesn't seem to compile anything :/

view this post on Zulip Paolo Giarrusso (Feb 18 2022 at 21:07):

Those instructions seem to imply the platform comes with cygwin.

view this post on Zulip Darij Grinberg (Feb 18 2022 at 21:07):

oof

view this post on Zulip Paolo Giarrusso (Feb 18 2022 at 21:08):

That is, the Windows platform should already include it

view this post on Zulip Darij Grinberg (Feb 18 2022 at 21:08):

ooooh

view this post on Zulip Darij Grinberg (Feb 18 2022 at 21:09):

not sure where i can find it then

view this post on Zulip Paolo Giarrusso (Feb 18 2022 at 21:09):

Can you find the folder where the platform is installed, and open it with explorer?

view this post on Zulip Darij Grinberg (Feb 18 2022 at 21:10):

yeah but there is nothing with "cygwin" in its name anywhere inside that folder

view this post on Zulip Paolo Giarrusso (Feb 18 2022 at 21:12):

Hm. Maybe search cygwin.bat through your computer? If that does not work, we’ll need some info from experts (I already tagged Michael Soegtrop)

view this post on Zulip Darij Grinberg (Feb 18 2022 at 21:12):

i have my own separate cygwin, that one sure has a cygwin.bat :)

view this post on Zulip Darij Grinberg (Feb 18 2022 at 21:12):

but i'd rather not run coq on that, as that would require an xserver for coqide and all the mess that comes with that

view this post on Zulip Paolo Giarrusso (Feb 18 2022 at 21:13):

That platform would give you make, and if you get coqc on the PATH you could compile both tools?

view this post on Zulip Paolo Giarrusso (Feb 18 2022 at 21:13):

sorry: combine.

view this post on Zulip Darij Grinberg (Feb 18 2022 at 21:14):

oh wow that seems to work!

view this post on Zulip Paolo Giarrusso (Feb 18 2022 at 21:15):

since you mentioned WSL above: you can of course install the Linux platform under WSL

view this post on Zulip Paolo Giarrusso (Feb 18 2022 at 21:15):

ah let’s discard WSL :-)

view this post on Zulip Paolo Giarrusso (Feb 18 2022 at 21:15):

re coqide, I think all it does to build code is call make

view this post on Zulip Paolo Giarrusso (Feb 18 2022 at 21:16):

_if coqide knows how to find it_, and I’m not sure how to do it if it doesn’t work out of the box

view this post on Zulip Darij Grinberg (Feb 18 2022 at 21:17):

yep it works!

view this post on Zulip Darij Grinberg (Feb 18 2022 at 21:17):

except now i see the code has rotten (library Omega is required and has not been found in the loadpath)

view this post on Zulip Darij Grinberg (Feb 18 2022 at 21:18):

looks like it's the least useful part of the code though

view this post on Zulip Darij Grinberg (Feb 18 2022 at 21:18):

nah, not quite...
make[1]: *** [Makefile:763: theories/Combi/tableau.vo] Error 127

view this post on Zulip Paolo Giarrusso (Feb 18 2022 at 21:19):

if that copy uses Omega it’s very old, but did you check out the latest version? I’m rechecking their github

view this post on Zulip Darij Grinberg (Feb 18 2022 at 21:19):

ah second time's the charm, apparently

view this post on Zulip Darij Grinberg (Feb 18 2022 at 21:19):

for the error 127 thing

view this post on Zulip Darij Grinberg (Feb 18 2022 at 21:19):

https://github.com/math-comp/Coq-Combi is half a year old

view this post on Zulip Darij Grinberg (Feb 18 2022 at 21:19):

but this is in a 3rd party include called alea

view this post on Zulip Darij Grinberg (Feb 18 2022 at 21:21):

don't think it's actually used

view this post on Zulip Paolo Giarrusso (Feb 18 2022 at 21:22):

Time to split this thread: most of the above is for the Coq-platform stream, now time for the math-comp stream

view this post on Zulip Paolo Giarrusso (Feb 18 2022 at 21:24):

Cyril Cohen is also very active here and he’d probably have an actual clue on the status.

view this post on Zulip Paolo Giarrusso (Feb 18 2022 at 21:25):

but it sounds like you’re mostly good to go @Darij Grinberg ?

view this post on Zulip Darij Grinberg (Feb 18 2022 at 21:25):

yep thank you!

view this post on Zulip Paolo Giarrusso (Feb 18 2022 at 21:26):

even if alea is not used, it’s not great if make fails out of the box, so that’s probably worth reporting.

view this post on Zulip Paolo Giarrusso (Feb 18 2022 at 21:26):

Anyway, good luck!

view this post on Zulip Enrico Tassi (Feb 18 2022 at 22:37):

FTR if you build the platform from sources it also installs a cygwin. If you install the windows installer the you get a native binary you can run without cygwin. Sure, if you want to run coq_makefile then you need a cygwin, but you should be able to use the coq from the installer.

view this post on Zulip Théo Zimmermann (Feb 19 2022 at 12:37):

It's interesting to read that a separate cygwin with make works fine with the Platform-installer-provided coqc and coq_makefile though.

view this post on Zulip Théo Zimmermann (Feb 19 2022 at 12:38):

We should probably improve the documentation to explain the various scenarios that people might be interested in and how things can work for them.

view this post on Zulip Darij Grinberg (Feb 19 2022 at 14:41):

yeah, I wasn't expecting that to work :)

view this post on Zulip Paolo Giarrusso (Feb 19 2022 at 15:01):

I expected that, just because cygwin and "native" programs can mostly interoperate via the PATH (not to say docs are complete, I agree with you).

view this post on Zulip Michael Soegtrop (Feb 19 2022 at 16:16):

@Théo Zimmermann : the hope was more that everybody switches to dune, so that makes gets obsolete. The main reason why one needs cygwin for make is that make needs a shell and a shell.

view this post on Zulip Théo Zimmermann (Feb 19 2022 at 16:21):

Yes, I agree that this is what we hope for the long-term. But we can expect the transition period to be several more years.


Last updated: Feb 04 2023 at 21:02 UTC