Hello everyone!
I’m working through the exercises in ‘Logical Foundations’ in the CoqIDE. I was able to import the definitions of the previous chapters till ‘Lists’. But I am not able to create a .vo file for ‘Lists’ to import for the next chapter.
I would really appreciate any help regarding this! Thank you :))
Hey Emily,
The theories in the logical foundations folder you downloaded and extracted need to be compiled / built before they can all work together (which makes the .vo files you require).
You should just be able to type the command make in a CLI interface (presuming you are on Linux, I don’t know how to process make-files on windows without using WSL) at the directory where you extracted the project in to do this.
Side note, if you ever need to recompile this project in the future, for example if you update the version of Coq you are using (which happened to me when I was using this resource to learn coq) you can run the command make clean followed by make to do this.
Hi Wolly,
Thank you so much for replying!
Yes, I realize that I have to compile the files somehow. I apologize for not mentioning beforehand that I work on a Windows system and not Linux :((
Right o!
So there two ways of building coq projects: one is using a makefile, and one is using dune. Both methods have better tooling support on Linux than windows out of the box, but you should be able to find the tools you need on Windows anyway.
In this instance what you need is a program that can build makefiles for windows, (so you need not worry about dune at the moment but you may need it for projects in the future). Lukily this problem is well documented and there are plenty of tools available! Pick a solution from this stackovreflow to get a program that can run make, and then you should be able to proceed as normal using the command line / power-shell to navigate to the project directory and then run make .
Whilst I have never used chocolaty I hear it is popular so going with the accepted answer in the linked resource seems like a good shout.
I would recommend at some point looking into the Windows Subsystem for Linux which essentially allows you to run a mini linux install inside of windows. This is great for running scientific computing / programming workflows (such as coq) as you get access to all of the linux tooling which these sorts of projects are typically based around.
I hope this helps, reply if you get stuck somewhere down the line as these things can be a little finicky before you get used to them!
Hi!
Thank you so much for helping out! I could install Chocolaty, but am unable to still run make. How exactly am I supposed to run the command?
Further, I had installed Oracle VM Virtual Box in my system and am running Ubuntu on it. I am still figuring out how to work with it but have run into some issues (I am unable to see any of the icons on the homepage and am not able to interact with the Start(?) icon). And so I wanted to program on CoqIDE till I can resolve the issue.
Ah fair!
I haven’t used VM software in a long time, so I am unable to help with the VM issue. I would say that WSL is (at least in my opinion) a nicer solution to work with than a full fat VM but ymmv.
Also, Coqide is available on Linux and is my IDE of choice, so you don’t necesserily have to move off from it if you decide you end up liking it. I know there is also emacs and VS Code support two if either of those take your fancy .
Great good job on installing Chocolaty! Did you run choco install make to ensure that make is on your system?
I’m going to quickly move over to my windows partition and try it for myself to see if If I can get everything to work / be able to give you more targeted instructions.
Hello!
Yes, I did run “choco install make” on Windows Powershell run as administrator.
By running the “make” command, do you mean I should open the ‘Lists’ file, and click on the ‘Compile’ and ‘Make’ options? I did try that, but it did not create the required .vo files.
Yes, I have tried to work on Coq with VS Code too, but ran into another trouble with installing the VsCoq language server. Things do run more smoothly in Linux ig :')
Hey, thanks for sticking with me:
Not exactly! according to the Windows usage instructions one needs to:
C:\my_coq_install_path\coq-shell.bat to open up a command line instance with access to the commands coqc and coqmakefile inside the shell.make in that folder.However, before that is done one needs to supply the CoqMakefile (this is an important file used by coq internally when building projects) . On Linux this is done with the command coq_makefile -f _CoqProject -o CoqMakefile and just works.
However, according to the Windows instructions I’ve just read in the documentation a different Windows-specific CoqMakefile is required and is supposed to be supplied in some supplementary add-on. Unfortunately searching through the git documentation and also my windows coq install I can’t find this addon. As a hail-mary I did try just proceeding with the linux version but that failed either due to incompatibility issues in the file makefile or the file CoqMakefile with windows.
I will open either an issue on git or ask a question in the Zulip chat / open a question here later today to see if the windows versions can be located.
I can only apologies for the frustration of this issue - I know from being a long term windows user how frustrating getting tools working properly on the platform can be when linux is the primary target.
In the meantime I cannot recommend enough setting up a WSL on your PC, grabbing the package opam and then installing coq through opam inside WSL. In my experience Coq is best supported on opam and opam best supported on Linux and once this is done anything you want to do with Coq should be pretty smooth sailing hence.
Although I can appreciate this issue is seemingly spiraling into some sort of cursed Sisyphean task getting a proper WSL workflow up and running will pay quickly pay dividends in your exploration of Coq and beyond.
I’m sorry I can’t be more help at the moment, hopefully I (or someone else) will have more useful info in the coming days.
Hello!
Thank you so much for continuing to help out :))
I will try to understand and execute the commands acc/to the Windows usage instructions.
Update: I deleted and re-installed Ubuntu on the VM. It started out working fine but then hung up again. I was able to resolve the issue by changing the Video Memory to 128MB after powering off Ubuntu. I could install Coq and am able to use it through VSCode (yay!). However, I ran into “Cannot find a physical path…” issue again, but will try to fix it using your answer in the first comment.
Thanks so much for helping!! :))
Hi again!
I am facing trouble with the .vo files again. I can see the .vo files for all chapters, but am getting an error when I try to run the command “From LF Require Export Basics”. Why would this be? Also, the CoqIDE shows an error for the computational equality expression: “=?”. Can anyone explain this?
PS - I am working with Coq inside VSCode.
Thanks!
What is the error you are getting now?
To run CoqIDE in WSL, you need to have an x server configured. On Windows 10, it was not easy to do so. (On Windows 11 it may be easier.)
I haven’t tried this yet, but I did see in Jan this year Microsoft added an update that makes setting up X much easier. Here is the link, It looks rather approachable now, but according to the pre-reqs it does explicitly require Win 11.
Hi!
So, currently, when I run the commands line by line in Induction.v, it shows me error in the line : “From LF Require Export Basics.”. The error goes away when I just write “Require Export Basics”, but then it does not import the definitions from Basics.v.
The error I’m seeing is this:
And furthermore, these:
[term expected] after ‘=’ (in [term])
Hi again,
The issue appeared to be resolved when you compile and make Basics.v, and then add the Induction.v file later, and then compile and make it and keep on doing so in order.
But the issue seems to be back again. And I get the following error when I go to the file Induction.v:
“Cannot find a physical path bound to logical path Basics with prefix LF.”
Can someone please help me figure this out?
Can I just check if you are trying this on Win or Ubuntu at the moment?
Hi! I am trying this on Ubuntu.
I am now getting the error message: Compiled library LF.Basics (in file /home/emily/coq/lf/Basics.vo) makes inconsistent assumptions over library Coq.Init.Ltac.
Also, I get an error message that opam is out of date.. please consider updating it, i tried to run both opam update and opam upgrade, but it does not work.
Hi!
I might have figured out the issue, but have not tried this yet… could the trouble have sprung up because I was first installing the Coq-Proof-Assistant as a snap package from the app store, and then when I was installing the VsCoq-Language-Server, I did it through the terminal using opam.
I am not sure, but I will uninstall the current Ubuntu on the VM, and set up a fresh one with all commands executed through the terminal using opam. I think the two installations of Coq packages/libraries interfere in some ways (?)
Its certainly possible.
Try with only one installed. If for whatever reason in the future you need more than one install of Coq the recommended way is to use opam with multiple switches but that’s an aside unrelated to getting LF working.
Okay, I’ll try this and let you know how it goes. Thank you so much!