Stream: Coq users

Topic: Using HoTT Library

Brandon Sisler (Nov 28 2022 at 15:45):

Hey all, I would like to use the HoTT library in the CoqIDE, but every time I try and import it I get the error message "Cannot find a physical path bound to logical path HoTT".
The solutions I have found say that once you have your _CoqProject file with the necessary info that it should work, but I have not found that to be the case. Has anyone run into this problem, and better yet, has anyone found a good solution? Thanks!

Karl Palmskog (Nov 28 2022 at 15:49):

did you install HoTT via the Coq Platform or opam (coq-hott package)?

Brandon Sisler (Nov 28 2022 at 15:51):

I am not sure, I thought that I did but how could I check?

Matthieu Sozeau (Nov 28 2022 at 16:07):

opam list if you're using opam should tell you

Brandon Sisler (Nov 28 2022 at 16:12):

I am not using opam but I just made sure that I do have it, I cloned it from GitHub.

Karl Palmskog (Nov 28 2022 at 16:16):

we highly recommend installing opam using instructions here and then, after initializing it (which means having an OCaml compiler), doing:

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

Brandon Sisler (Nov 28 2022 at 16:17):

You're the boss, it will be just a moment.

Karl Palmskog (Nov 28 2022 at 16:17):

installing HoTT directly from the GitHub repo is in my view an experts only thing

Karl Palmskog (Nov 28 2022 at 16:18):

also, if you don't mind getting a bunch of other packages, a more automated option is via the Coq Platform (it will install opam for you, along with Coq and packages including HoTT)

Brandon Sisler (Nov 28 2022 at 17:03):

That's what I ended up doing, although the error has persisted. I am also still having difficulty locating opam.
Is there a path that I should follow to find it?

Karl Palmskog (Nov 28 2022 at 17:23):

if you installed via the Coq Platform, the opam executable should be somewhere in your path (mine ended up in $(HOME)/bin)

Brandon Sisler (Nov 29 2022 at 01:04):

Aha! Found it! Should I still install OCaml?

Paolo Giarrusso (Nov 29 2022 at 02:13):

the platform has enough (and it probably already installed OCaml)

Brandon Sisler (Nov 29 2022 at 02:43):

Yes, looks like it! Alright, so now I can even see the HoTT library, and yet, I cannot import it, I have the same error!

Paolo Giarrusso (Nov 29 2022 at 05:27):

My guess: you're using the same CoqIDE installation as before, aren't you? Can you run opam now? If yes, try running opam install coqide, and if that succeeds, uninstall the CoqIDE you're using.

If you write more on how you installed CoqIDE before, we can guess better if that's the problem.

Paolo Giarrusso (Nov 29 2022 at 05:28):

The reason is (a) compiled libraries can't be shared between separate Coq installations (b) CoqIDE installers come with their own Coq installation, but where packages cannot be installed (c) the platform comes with a regular Coq installation where libraries can be installed.

Brandon Sisler (Nov 30 2022 at 01:35):

I can locate it, but it will not open or run. I tried to just download it after that anyways to see what happened, but I cannot find a way to do that on a windows computer.

Ali Caglayan (Nov 30 2022 at 14:32):

How are you importing the HoTT library?

Brandon Sisler (Nov 30 2022 at 14:37):

I have been typing "Require Import HoTT."
I have also attempted "From HoTT Require Import Basic."

Ali Caglayan (Nov 30 2022 at 14:38):

Do you have a which command? If so, could you show what which coqc and which coqide give you?

Karl Palmskog (Nov 30 2022 at 14:39):

I think you need to do at least:

From HoTT Require Import Basics.

For sure, Require Import HoTT. will not work (this would mean Coq's Stdlib contains a HoTT module, which it doesn't).

Ali Caglayan (Nov 30 2022 at 14:40):

Also there is a file in the HoTT library called HoTT.v which reexports most of the library. If you want to get using it you can do Require Import HoTT.HoTT. or more correctly From HoTT Require Import HoTT.

Ali Caglayan (Nov 30 2022 at 14:41):

If those don't work however, let us know what which says, my suspicion is that there may be a mismatch between your coq and coqide version.

Karl Palmskog (Nov 30 2022 at 14:42):

one way to test if Coq itself works is to put the HoTT require-import into a file file.v and run coqc file.v. If no errors, CoqIDE is likely the culprit.

Michael Soegtrop (Nov 30 2022 at 15:00):

@Brandon Sisler : a few questions / notes:

• which OS are or using?
• did you install Coq Platform via the "compile from sources" scripts or via an installer?
• as far as I know HoTT still requires -noinit -indices-matter options.

Michael Soegtrop (Nov 30 2022 at 15:01):

Also which version of Coq Platform did you use?

Brandon Sisler (Nov 30 2022 at 15:03):

@Michael Soegtrop
I am using Windows 10, and installed the Coq Platform via an installer (version 8.16).
And this is true, although I have done as the library asked and created a
_CoqProject file with the relevant text.

Brandon Sisler (Nov 30 2022 at 15:06):

@Ali Caglayan I cannot find a way to use the which command, since I cannot get opam to work, nor will it run in the CoqIDE.

Brandon Sisler (Nov 30 2022 at 15:07):

@Karl Palmskog From HoTT Require Import Basics. has given me an interesting new error
Notation "~ _" is already defined at level 75 with arguments constr at level 75 while it is now required to be at level 35 with arguments constr at level 35.

Karl Palmskog (Nov 30 2022 at 15:07):

which is a Unix command

Ali Caglayan (Nov 30 2022 at 15:12):

Brandon Sisler said:

Karl Palmskog From HoTT Require Import Basics. has given me an interesting new error
Notation "~ _" is already defined at level 75 with arguments constr at level 75 while it is now required to be at level 35 with arguments constr at level 35.

OK that is working now.

Ali Caglayan (Nov 30 2022 at 15:13):

But you need to run coqide with -noinit -indices-matter

Ali Caglayan (Nov 30 2022 at 15:13):

See the HoTT repo README.md about that

Ali Caglayan (Nov 30 2022 at 15:13):

You can put those args in your _CoqProject too

Michael Soegtrop (Nov 30 2022 at 15:15):

@Brandon Sisler : in case you used the installer, there is a CoqIDE under something like C:\Program Files\CoqXYZ\bin. When you start this CoqIDE, it should work.

Michael Soegtrop (Nov 30 2022 at 15:19):

One more note on _CoqProject_ : Afaik CoqIDE reads the file when it opens a file. When you create a new file and save it, it doesn't work. So create a .v file in the same folder as _CoqProject_ and open it in CoqIDE.

Michael Soegtrop (Nov 30 2022 at 17:01):

@Brandon Sisler : does it work now?

Brandon Sisler (Nov 30 2022 at 17:06):

Sorry, I was away, I have done what you said but I still cannot get it to run, and I have the same error as before, even with the project file and the suggested startup.

Kenji Maillard (Nov 30 2022 at 17:09):

@Brandon Sisler Is the content of your _CoqProject as indicated in the HoTT readme ?

-arg -noinit
-arg -indices-matter

Brandon Sisler (Nov 30 2022 at 17:17):

Yes, that's right

Karl Palmskog (Nov 30 2022 at 17:59):

I recommend having a _CoqProject like this (assuming your file which require-imports HoTT is called file.v):

-arg -noinit
-arg -indices-matter
file.v

Then, you can run:

coq_makefile -f _CoqProject -o Makefile
make

This should compile file.v without errors.

Michael Soegtrop (Nov 30 2022 at 18:00):

@Karl Palmskog : these instructions won't work easily on Windows ... (no make).

Karl Palmskog (Nov 30 2022 at 18:01):

sigh, no make and no Dune (for Coq), that rules out nearly every sensible way of organizing a Coq project

Michael Soegtrop (Nov 30 2022 at 18:01):

dune is there ...

Michael Soegtrop (Nov 30 2022 at 18:02):

In the old days there was a make, but people found it impossible to use without shell, grep, sed, ...

Michael Soegtrop (Nov 30 2022 at 18:02):

So I removed it a long time ago (8.7 or so).

Karl Palmskog (Nov 30 2022 at 18:02):

but can Dune actually compile Coq? I thought Dune didn't work at all due to no OCaml

Paolo Giarrusso (Nov 30 2022 at 18:03):

In any case, it seems that almost everything in coqide, except that coqide did not pick up _CoqProject

Paolo Giarrusso (Nov 30 2022 at 18:03):

A working build is orthogonal?

Michael Soegtrop (Nov 30 2022 at 18:03):

Actually I don't know. Wasn't this dependency removed (need for OCaml at run time)?

Michael Soegtrop (Nov 30 2022 at 18:04):

Anyway, I was about to make the 2022.09.1 Windows builds, so I can have a look.

Karl Palmskog (Nov 30 2022 at 18:04):

if it can work from CLI with _CoqProject and the HoTT options, then at least the problems are isolated to CoqIDE

Paolo Giarrusso (Nov 30 2022 at 18:05):

But the error seems to prove that it'd work that way

Paolo Giarrusso (Nov 30 2022 at 18:06):

And troubleshooting the coqide lookup requires knowing the coqide lookup rules for coqproject

Paolo Giarrusso (Nov 30 2022 at 18:06):

(anybody who knows them could help)

Michael Soegtrop (Nov 30 2022 at 18:07):

As I said I think the issue is that people create a new file and save it. This does not work. CoqIDE reads the _CoqProject_ file only when it opens a file.

Michael Soegtrop (Nov 30 2022 at 18:14):

Just a note: I will do a screen sharing session with @Brandon Sisler a bit later today to make sure nothing got messed up in Coq Platform (I am about to make a new release so better double check).

Michael Soegtrop (Dec 01 2022 at 14:11):

I had a quick screen sharing session with Brandon. The issue was that he created the _CoqProject file with Notepad, so it got a hidden .txt extension (Windows by default hides extensions for registered applications). Removing the .txt extension solved this.

Michael Soegtrop (Dec 01 2022 at 14:11):

@Paolo Giarrusso @Karl Palmskog @Ali Caglayan : if you can think of a good place to document this, please let me know.

Michael Soegtrop (Dec 01 2022 at 17:50):

Btw.: I changed the smoke test kit creation such that for packages which need options a _CoqProject file is automatically creates. So one can simply run an example from the smoke test kit in CoqIDE and e,g, copy the _CoqProject file from the smoke test kit. This should simplify helping users with IDE issues.

Ali Caglayan (Dec 01 2022 at 20:06):

Michael Soegtrop said:

Paolo Giarrusso Karl Palmskog Ali Caglayan : if you can think of a good place to document this, please let me know.

I would add a note here:

• https://coq.inria.fr/refman/practical-tools/utilities.html?highlight=_coqproject#building-a-coq-project-with-coq-makefile
  Something like:

.. note::
   Windows users should be especially careful that their `_CoqProject` file is named correct and that there is no hidden `.txt` extension, as Windows can hide this.

cc @Jim Fehrle

Jim Fehrle (Dec 01 2022 at 20:29):

I'll add a note to that effect. I think it belongs in the new "Coq Configuration Basics" section that will appear in 8.17, which you can peruse here. I would put the note in the "Building a project with _CoqProject (overview)" subsection.

Ali Caglayan (Dec 01 2022 at 20:40):

I would imagine a user that runs into this issue searches for _CoqProject in the refman. The first result in the search is the location I linked. It wouldn't hurt to link it in multiple places. Or perhaps we should start a list of Gotchas for Windows?

Jim Fehrle (Dec 01 2022 at 20:58):

Let's keep this simple. I thought I'd put in a quick PR, but it's a low priority for me. If you want to submit a PR with a list of "gotchas" and places to link to it, go ahead and I will review it. I'm sceptical (but open minded) that that's a good approach. What other items would you include? Linking in multiple places is a two edged sword: it is more text to read in each place the link appears. Also it's very basic info--it's something users will quickly learn if they don't already know about it. Nor is it clear how many Windows Coq users don't already know about this.

You should be looking at the 8.17 documentation that I linked to above. I expect we would not update this in an 8.16.2 version. The subsection I mentioned is the first subsection with_CoqProect in the title and almost the first reference to _CoqProject in that chapter.

Paolo Giarrusso (Dec 01 2022 at 21:30):

FWIW this isn't Windows-specific, all OSes hide extensions by default.

Paolo Giarrusso (Dec 01 2022 at 21:34):

As a separate note, typical "open file/open project" flows (in many OSes) would actually let you validate that the project is correctly set up and appropriate files are found. Of course, that would be more work, but also be more effective :-|

Jim Fehrle (Dec 01 2022 at 21:55):

Paolo, where does Linux hide the extension? bash and vi, etc. show/require the extensions.

More validation is a good idea. Since there are so many potential improvements, we should be systematic in identifying which ones provide the most value to users with the least effort. @Théo Zimmermann and I were recently discussing creating a list of the most valuable improvements.

Paolo Giarrusso (Dec 02 2022 at 00:11):

sorry for the brain fart (now crossed), let me try again: some graphical file managers on OSes other than Windows also hide extensions. On Mac IIRC it's a default (I flipped it years ago), on Linux I think it varies.

Paolo Giarrusso (Dec 02 2022 at 00:12):

(haven't used Linux in ages but this still seems to arise: https://forums.linuxmint.com/viewtopic.php?t=218705 ?)

Paolo Giarrusso (Dec 02 2022 at 00:13):

but I'm not confident, especially on how common this is.

Paolo Giarrusso (Dec 02 2022 at 00:13):

:+1: on prioritization

Karl Palmskog (Dec 02 2022 at 07:19):

to my knowledge, Linux and BSD are neutral at kernel level to file extensions. But then specific *Nix applications such as file managers may hide or take into account file extensions.

Karl Palmskog (Dec 02 2022 at 07:20):

but I thought the long-term plan was to throw out _CoqProject and rely on something like dune coq in most IDEs. On the other hand, dune and dune-project should also not have file extensions.

Paolo Giarrusso (Dec 02 2022 at 18:35):

yeah, AFAICT even on windows file managers are the main problem: if they hide the extension, the problem is hidden as well

Last updated: Sep 28 2023 at 10:01 UTC