Franklin Pezzuti Dyer (May 20 2022 at 23:00): Franklin Pezzuti Dyer (May 20 2022 at 23:00):Hi all! I've only been using Coq for a little while (using the CoqIDE on MacOS with M1) and I've just recently written enough code that it's worth separating my code into different files. However, once I started trying to find out how to import functions and lemmas from one file to another, I ended up pulling my hair out.
Right now, my file structure looks like this:
.
|-- basic_arithmetic.v
|-- divisibility.v
In basic_arithmetic.v, I've written several lemmas regarding e.g. commutativity and associativity of addition and multiplication, which I would like to use in divisibility.v, and both files are open in the CoqIDE.
Is there a simple way of importing my lemmas from basic_arithmetic.v for use in divisibility.v? Can I use something simple like Require Import basic_arithmetic.? (I know this does not work - the IDE gives the error "unable to locate library basic_arithmetic".)
Note: I've found a couple of relevant help/documentation pages online by googling, but none of their solutions have worked for me. I've tried several slight variations on Require Import and Add LoadPath.
Paolo Giarrusso (May 20 2022 at 23:13):You shouldn't use LoadPath, you should use Require Import, but you'll need to either switch to Emacs or add some build infrastructure, likely using coq_makefile
Paolo Giarrusso (May 20 2022 at 23:18):For a minimal example, move your files under theories, add the following to _CoqProject:
-R theories project_name
then run
coq_makefile -o Makefile -f _CoqProject $(find theories -name '*.v')
make -j4
rerun the make command when changing the code, and rerun coq_makefile when adding new files
Paolo Giarrusso (May 20 2022 at 23:21):one can automate this a bit more, but this is the basic idea and should get you unstuck
Paolo Giarrusso (May 20 2022 at 23:25):the Coq manual does give tips on the next level of automation, FWIW, even if it might not be extremely clear: https://coq.inria.fr/refman/practical-tools/utilities.html#building-a-coq-project-with-coq-makefile
Franklin Pezzuti Dyer (May 20 2022 at 23:33):Paolo Giarrusso said:
For a minimal example, move your files under
theories, add the following to_CoqProject:-R theories project_namethen run
coq_makefile -o Makefile -f _CoqProject $(find theories -name '*.v') make -j4
Thanks! Once I've done this, what is the syntax for importing my stuff into divisibility.v? Should I use something like Require Import project_name? I'm trying this right now, and having no luck with it.
Paolo Giarrusso (May 21 2022 at 04:26):Require Import basic_arithmetic. or Require Import project_name.basic_arithmetic. would work.
Franklin Pezzuti Dyer (May 22 2022 at 21:04):Paolo Giarrusso said:
Require Import basic_arithmetic.orRequire Import project_name.basic_arithmetic.would work.
After following your instructions and wrangling a few version control issues involving OCaml, I've ended up with a completely different error:
The file /Users/franklindyer/Coq-play/theories/testFile1.vo contains library
testFile1 and not library project_name.testFile1.
any ideas what this one means?
Franklin Pezzuti Dyer (May 22 2022 at 21:07):For context, I decided to stop trying with basic_arithmetic and instead try to get a basic example working. In theories/testFile1.v, I have
Definition a : nat := 3.
and in testFile2.v, I have
Require Import testFile1.
Definition b := a.
you should always use -Q or -R option when compiling a project with coqc/coqtop. If you leave them out, you won't have a toplevel name like project_name. I highly recommend setting up your project like it's done here: https://github.com/coq-community/jmlcoq/
.. and simply changing JML to the top-level name you want, not least in _CoqProject.
Karl Palmskog (May 22 2022 at 21:10):using coqc -Q <dir> <coqname/path> instead of -R <dir> <coqname/path> can be useful, since it prevents referring to other files in the project by unqualified names
Franklin Pezzuti Dyer (May 22 2022 at 21:18):Alright, I've tried to set this up as similarly as possible to your file structure, but now I'm getting Cannot find a physical path bound to logical path
testFile1.
Franklin Pezzuti Dyer (May 22 2022 at 21:19):(when I attempt to use Require Import testFile1. in testFile2)
Li-yao (May 22 2022 at 21:21):where are the files and what commands are you compiling them with exactly
Karl Palmskog (May 22 2022 at 21:22):@Franklin Pezzuti Dyer if you are indeed using -Q as in that example project, then you need to do:
Require Import project_name.testFile1.
an idiom many people use is also:
From project_name Require Import testFile1.
my file structure is
Coq-proj
|- _CoqProject
|- testFile2.v
|- theories
|- testFile1.v
and I am using the commands suggested by @Paolo Giarrusso to compile, except that my _CoqProject file now uses -Q instead of -R
Franklin Pezzuti Dyer (May 22 2022 at 21:26):Karl Palmskog said:
Franklin Pezzuti Dyer if you are indeed using
-Qas in that example project, then you need to do:Require Import project_name.testFile1.
Got it. Now that I do this, I'm getting the following error:
Compiled library MyProj.testFile1 (in file /Users/franklindyer/Coq-proj/theories/testFile1.vo) makes inconsistent assumptions over library Coq.Init.Ltac
...which, if my googling has not led me astray, means that I'm having more version issues. But I'm not sure why this would be the case, since I'm using the 8.15.1CoqIDE, and running coqc -v gives The Coq Proof Assistant, version 8.15.1.
Karl Palmskog (May 22 2022 at 21:27):if you have a theories directory, you should always put all files in there:
Coq-proj
|- _CoqProject
|- theories
|- testFile1.v
|- testFile2.v
and then your _CoqProject file should say:
-Q theories project_name
theories/testFile1.v
theories/testFile2.v
before jumping into CoqIDE, I highly recommend compiling the whole project first, assuming you are using the boilerplate Makefile from the example project:
cd path-to-Coq-proj
make clean
make
Karl Palmskog said:
before jumping into CoqIDE, I highly recommend compiling the whole project first, assuming you are using the boilerplate
Makefilefrom the example project:cd path-to-Coq-proj make clean make
Okay got it, I'm using the same MakeFile. When I try to compile without using the IDE, I get the following error:
File "./theories/testFile2.v", line 1, characters 0-25:
Error: Cannot find a physical path bound to logical path testFile1.
make[2]: *** [theories/testFile2.vo] Error 1
make[1]: *** [all] Error 2
make: *** [all] Error 2
so it looks like something is still wrong in testFile2. But I'm not sure what "cannot find a physical path bound to logical path" means...
Karl Palmskog (May 22 2022 at 21:37):did you change to Require Import project_name.testFile1.?
Franklin Pezzuti Dyer (May 22 2022 at 21:39):Oho, it looks like I did that in the IDE but it didn't save my change. Now it compiles! :D
Karl Palmskog (May 22 2022 at 21:39):the physical path is <local-dirs>/theories/testFile1.v, for example, while it seems like you want the logical path to be project_name.testFile1. Coq needs to be aware of this mapping, so we pass it through -R or -Q
Franklin Pezzuti Dyer (May 22 2022 at 21:40):Fantastic. I'm glad it will compile from the command line now - the IDE still doesn't like it though, it's giving that inconsistent assumptions over library Coq.Init.Ltac error again.
Karl Palmskog (May 22 2022 at 21:41):inconsistent assumptions stuff is a sign that you have stale .vo files somewhere
Karl Palmskog (May 22 2022 at 21:41):I advise cleaning out all .vo files in theories and compiling from scratch
Franklin Pezzuti Dyer (May 22 2022 at 21:42):Hmm, running make clean and make again does not fix the issue
Franklin Pezzuti Dyer (May 22 2022 at 21:42):and I checked in between that there were no leftover .vo files
Karl Palmskog (May 22 2022 at 21:42):make clean can only clean out .vo files that are listed in _CoqProject
Karl Palmskog (May 22 2022 at 21:42):you may have some other .vo files laying around from before
Franklin Pezzuti Dyer (May 22 2022 at 21:43):I checked for other .vo files manually after running make clean
Franklin Pezzuti Dyer (May 22 2022 at 21:43):all I had left in that folder were testFile1.v and testFile2.v
Karl Palmskog (May 22 2022 at 21:44):OK, if it only happens with the IDE and not via command-line compilation, then something may have gone wrong during IDE installation
Karl Palmskog (May 22 2022 at 21:44):the standard advice is to try an alternative IDE and see if the error persists. If other IDEs don't have the errror, then I'd try reinstalling the first IDE
Karl Palmskog (May 22 2022 at 21:45):for example, you could try VsCode+VsCoq
Franklin Pezzuti Dyer (May 22 2022 at 21:45):Ahhh. If I launch the IDE by running coqide, it works. But if I launch it by clicking on the app, it does not
Karl Palmskog (May 22 2022 at 21:46):yeah, the two may actually be different executables?
Karl Palmskog (May 22 2022 at 21:46):I always trust the command line more than buttons
Franklin Pezzuti Dyer (May 22 2022 at 21:46):yup. that explains it
Franklin Pezzuti Dyer (May 22 2022 at 21:46):Hahaha fair
Franklin Pezzuti Dyer (May 22 2022 at 21:48):Thank you so much for your help! Almost certainly would not have figured this out otherwise. :grinning_face_with_smiling_eyes:
Paolo Giarrusso (May 22 2022 at 22:33):@Karl Palmskog is it expected that different binaries for the same version are incompatible? I’ve seen that when checksums included timestamps, but recent discussions here seemed to suggest that might not be the case?
Karl Palmskog (May 22 2022 at 22:39):I don't think checksums include timestamps. When I have problems with "inconsistent assumptions", it's always been due to some stale .vo file in the middle of some dependency chain. That is, the actual content of some file changed, not just its timestamp.
Paolo Giarrusso (May 22 2022 at 22:42):I'm confident I've seen otherwise in the past, _but_ I've just found https://github.com/coq/coq/pull/13863.
Paolo Giarrusso (May 22 2022 at 22:44):(I consider my question solved, but any further discussion is probably best kept for https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/how.20portable.20are.20.2Evo.20files.3F)
João Mendes (Aug 15 2023 at 20:46):Reopening this topic because I am having the same problem and didn't manage to solve it.
My folder structure is:
test
|- _CoqProject
|- theories
|- file1.v
|- file2.v
The content of the _CoqProject file is
-Q theories compile_test
theories/file1.v
theories/file2.v
My goal is to import the functions from file1 to file2.
The commands I executed in the terminal were:
coq_makefile -o Makefile -f _CoqProject $(find theories -name '*.v')
make
And, inside the theories folder,
coqtop < file2.v
When the header of file2 is
From compile_test Require Import file1.
I get the following message in stderr
Welcome to Coq 8.15.0
Coq < Toplevel input, characters 0-39:
> From compile_test Require Import file1.
> ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: Cannot find a physical path bound to logical path
file1 with prefix compile_test.
And when the header of file2 is
From Require Import compile_test.file1.
I get the following message in stderr
Welcome to Coq 8.15.0
Coq < Toplevel input, characters 0-34:
> Require Import compile_test.file1.
> ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: Cannot find a physical path bound to logical path compile_test.file1.
I recommend not using coqtop directly, since it will typically only work with proper -Q .../-R ... options. Consider using a Makefile like this one: https://github.com/coq-community/huffman/blob/master/Makefile
... and then run make in the directory with the Makefile (same as where _CoqProject is located).
Paolo Giarrusso (Aug 15 2023 at 20:56):Karl is 100% right. coqtop should work if you also pass -Q theories compile_test, but the point of running coq_makefile (by hand, or the way Karl suggests) is that you can then just run make to build code.
João Mendes (Aug 15 2023 at 21:18):I don't know if there is another to run a Coq code in terminal besides coqtop. But my motivation for this is that I am using Python to analyze log lines of a platform that has Coq in its core. So, I want to execute Coq codes, extracted from these logs, in this same Python script.
It worked now using such Makefile and running the command with the proper arguments
coqtop -Q . compile_test < file2.v
Thanks!
Karl Palmskog (Aug 15 2023 at 21:21):I'd recommend looking into one or more of these projects if you want to interact with Coq from Python:
Karl Palmskog (Aug 15 2023 at 21:22):executing Coq code manually (or even automatically) via coqtop is not likely to end well, due to its limitations
Karl Palmskog (Aug 15 2023 at 21:25):to give one example: Coq's lexer and parser can change with the execution of any sentence.
João Mendes (Aug 15 2023 at 21:28):Hmmm fair enough
Karl Palmskog (Aug 15 2023 at 21:30):some scripts are also available here that can turn a "Coq project" into a single .v file, if the right invocations are used: https://github.com/JasonGross/coq-tools
João Mendes (Aug 15 2023 at 21:44):Many thanks for the recommendations! I'll surely take a look on them
Last updated: Sep 23 2023 at 08:01 UTC