Darij Grinberg (Feb 18 2022 at 19:59): 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?
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?
Darij Grinberg (Feb 18 2022 at 20:01):ah! but can I find the .v files itself somewhere in the hierarchy?
Darij Grinberg (Feb 18 2022 at 20:02):yeah the imports work
Darij Grinberg (Feb 18 2022 at 20:02):oh in user-contrib
Darij Grinberg (Feb 18 2022 at 20:03):is this where I put my own .vs too?
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).
Darij Grinberg (Feb 18 2022 at 20:06):Oh, it is what I wanted to ask a few questions later :) thank you!
Darij Grinberg (Feb 18 2022 at 20:07):to be specific, I want to import files from a project in the same project
Darij Grinberg (Feb 18 2022 at 20:07):i think all its dependencies are in the platform already, but it is not
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.
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
Gaëtan Gilbert (Feb 18 2022 at 20:08):user-contrib is where projects from "users" get installed by coq_makefile make install
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?
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
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
Darij Grinberg (Feb 18 2022 at 20:09):maybe just transferring the github owner
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
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?
Darij Grinberg (Feb 18 2022 at 20:11):ideally, both
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).
Darij Grinberg (Feb 18 2022 at 20:15):Cloned it, but where should I run make from? From WSFL?
Ana de Almeida Borges (Feb 18 2022 at 20:16):From the main directory, the one where the makefile is
Darij Grinberg (Feb 18 2022 at 20:17):from what kind of console?
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?
Darij Grinberg (Feb 18 2022 at 20:18):ah, is the output system-independent?
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.
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.
Ana de Almeida Borges (Feb 18 2022 at 20:20):(assuming you are using CoqIDE)
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
Darij Grinberg (Feb 18 2022 at 20:21):anyway thanks a lot for answering my first few questions!
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.
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"
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
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
Paolo Giarrusso (Feb 18 2022 at 20:56):or check if the platform comes with tools to set the right build environment
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.”
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.
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?
Darij Grinberg (Feb 18 2022 at 21:04):oh! can I use cygwin independently of how i installed the coq platform?
Darij Grinberg (Feb 18 2022 at 21:04):or do I need to install the Linux platform under cygwin for that?
Darij Grinberg (Feb 18 2022 at 21:05):I don't think I have a cygwin bat anywhere in my coq platform
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
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 :/
Paolo Giarrusso (Feb 18 2022 at 21:07):Those instructions seem to imply the platform comes with cygwin.
Darij Grinberg (Feb 18 2022 at 21:07):oof
Paolo Giarrusso (Feb 18 2022 at 21:08):That is, the Windows platform should already include it
Darij Grinberg (Feb 18 2022 at 21:08):ooooh
Darij Grinberg (Feb 18 2022 at 21:09):not sure where i can find it then
Paolo Giarrusso (Feb 18 2022 at 21:09):Can you find the folder where the platform is installed, and open it with explorer?
Darij Grinberg (Feb 18 2022 at 21:10):yeah but there is nothing with "cygwin" in its name anywhere inside that folder
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)
Darij Grinberg (Feb 18 2022 at 21:12):i have my own separate cygwin, that one sure has a cygwin.bat :)
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
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?
Paolo Giarrusso (Feb 18 2022 at 21:13):sorry: combine.
Darij Grinberg (Feb 18 2022 at 21:14):oh wow that seems to work!
Paolo Giarrusso (Feb 18 2022 at 21:15):since you mentioned WSL above: you can of course install the Linux platform under WSL
Paolo Giarrusso (Feb 18 2022 at 21:15):ah let’s discard WSL :-)
Paolo Giarrusso (Feb 18 2022 at 21:15):re coqide, I think all it does to build code is call make
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
Darij Grinberg (Feb 18 2022 at 21:17):yep it works!
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)
Darij Grinberg (Feb 18 2022 at 21:18):looks like it's the least useful part of the code though
Darij Grinberg (Feb 18 2022 at 21:18):nah, not quite...
make[1]: *** [Makefile:763: theories/Combi/tableau.vo] Error 127
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
Darij Grinberg (Feb 18 2022 at 21:19):ah second time's the charm, apparently
Darij Grinberg (Feb 18 2022 at 21:19):for the error 127 thing
Darij Grinberg (Feb 18 2022 at 21:19):https://github.com/math-comp/Coq-Combi is half a year old
Darij Grinberg (Feb 18 2022 at 21:19):but this is in a 3rd party include called alea
Darij Grinberg (Feb 18 2022 at 21:21):don't think it's actually used
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
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.
Paolo Giarrusso (Feb 18 2022 at 21:25):but it sounds like you’re mostly good to go @Darij Grinberg ?
Darij Grinberg (Feb 18 2022 at 21:25):yep thank you!
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.
Paolo Giarrusso (Feb 18 2022 at 21:26):Anyway, good luck!
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.
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.
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.
Darij Grinberg (Feb 19 2022 at 14:41):yeah, I wasn't expecting that to work :)
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).
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.
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: Dec 01 2023 at 06:01 UTC