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!
did you install HoTT via the Coq Platform or opam (
I am not sure, I thought that I did but how could I check?
opam list if you're using opam should tell you
I am not using opam but I just made sure that I do have it, I cloned it from GitHub.
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
You're the boss, it will be just a moment.
installing HoTT directly from the GitHub repo is in my view an experts only thing
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)
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?
if you installed via the Coq Platform, the
opam executable should be somewhere in your path (mine ended up in
Aha! Found it! Should I still install OCaml?
the platform has enough (and it probably already installed OCaml)
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!
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.
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.
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.
How are you importing the HoTT library?
I have been typing "Require Import HoTT."
I have also attempted "From HoTT Require Import Basic."
Do you have a
which command? If so, could you show what
which coqc and
which coqide give you?
I think you need to do at least:
From HoTT Require Import Basics.
Require Import HoTT. will not work (this would mean Coq's Stdlib contains a
HoTT module, which it doesn't).
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.
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.
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.
@Brandon Sisler : a few questions / notes:
Also which version of Coq Platform did you use?
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.
@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.
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.
which is a Unix command
Brandon Sisler said:
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.
But you need to run coqide with -noinit -indices-matter
See the HoTT repo README.md about that
You can put those args in your _CoqProject too
@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.
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.
@Brandon Sisler : does it work now?
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.
@Brandon Sisler Is the content of your
_CoqProject as indicated in the HoTT readme ?
-arg -noinit -arg -indices-matter
Yes, that's right
I recommend having a
_CoqProject like this (assuming your file which require-imports HoTT is called
-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.
@Karl Palmskog : these instructions won't work easily on Windows ... (no make).
sigh, no make and no Dune (for Coq), that rules out nearly every sensible way of organizing a Coq project
dune is there ...
In the old days there was a make, but people found it impossible to use without shell, grep, sed, ...
So I removed it a long time ago (8.7 or so).
but can Dune actually compile Coq? I thought Dune didn't work at all due to no OCaml
In any case, it seems that almost everything in coqide, except that coqide did not pick up _CoqProject
A working build is orthogonal?
Actually I don't know. Wasn't this dependency removed (need for OCaml at run time)?
Anyway, I was about to make the 2022.09.1 Windows builds, so I can have a look.
if it can work from CLI with _CoqProject and the HoTT options, then at least the problems are isolated to CoqIDE
But the error seems to prove that it'd work that way
And troubleshooting the coqide lookup requires knowing the coqide lookup rules for coqproject
(anybody who knows them could help)
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.
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).
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.
@Paolo Giarrusso @Karl Palmskog @Ali Caglayan : if you can think of a good place to document this, please let me know.
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.
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:
.. 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
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.
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?
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.
FWIW this isn't Windows-specific,
all OSes hide extensions by default.
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 :-|
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.
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.
(haven't used Linux in ages but this still seems to arise: https://forums.linuxmint.com/viewtopic.php?t=218705 ?)
but I'm not confident, especially on how common this is.
:+1: on prioritization
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.
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-project should also not have file extensions.
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