Stream: Coq users

Topic: Importing functions/lemmas from one Coq file to another?


view this post on Zulip 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".)

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Paolo Giarrusso (May 20 2022 at 23:19):

rerun the make command when changing the code, and rerun coq_makefile when adding new files

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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_name

then 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.

view this post on Zulip Paolo Giarrusso (May 21 2022 at 04:26):

Require Import basic_arithmetic. or Require Import project_name.basic_arithmetic. would work.

view this post on Zulip Franklin Pezzuti Dyer (May 22 2022 at 21:04):

Paolo Giarrusso said:

Require Import basic_arithmetic. or Require 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.

view this post on Zulip Franklin Pezzuti Dyer (May 22 2022 at 21:04):

any ideas what this one means?

view this post on Zulip 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.

view this post on Zulip Karl Palmskog (May 22 2022 at 21:08):

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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Franklin Pezzuti Dyer (May 22 2022 at 21:19):

(when I attempt to use Require Import testFile1. in testFile2)

view this post on Zulip Li-yao (May 22 2022 at 21:21):

where are the files and what commands are you compiling them with exactly

view this post on Zulip 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.

view this post on Zulip Karl Palmskog (May 22 2022 at 21:24):

an idiom many people use is also:

From project_name Require Import testFile1.

view this post on Zulip Franklin Pezzuti Dyer (May 22 2022 at 21:24):

my file structure is

Coq-proj
|- _CoqProject
|- testFile2.v
|- theories
    |- testFile1.v

view this post on Zulip Franklin Pezzuti Dyer (May 22 2022 at 21:25):

and I am using the commands suggested by @Paolo Giarrusso to compile, except that my _CoqProject file now uses -Q instead of -R

view this post on Zulip Franklin Pezzuti Dyer (May 22 2022 at 21:26):

Karl Palmskog said:

Franklin Pezzuti Dyer if you are indeed using -Q as 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.

view this post on Zulip 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

view this post on Zulip Karl Palmskog (May 22 2022 at 21:28):

and then your _CoqProject file should say:

-Q theories project_name

theories/testFile1.v
theories/testFile2.v

view this post on Zulip Karl Palmskog (May 22 2022 at 21:29):

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

view this post on Zulip Franklin Pezzuti Dyer (May 22 2022 at 21:36):

Karl Palmskog said:

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

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...

view this post on Zulip Karl Palmskog (May 22 2022 at 21:37):

did you change to Require Import project_name.testFile1.?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Karl Palmskog (May 22 2022 at 21:41):

inconsistent assumptions stuff is a sign that you have stale .vo files somewhere

view this post on Zulip Karl Palmskog (May 22 2022 at 21:41):

I advise cleaning out all .vo files in theories and compiling from scratch

view this post on Zulip Franklin Pezzuti Dyer (May 22 2022 at 21:42):

Hmm, running make clean and make again does not fix the issue

view this post on Zulip Franklin Pezzuti Dyer (May 22 2022 at 21:42):

and I checked in between that there were no leftover .vo files

view this post on Zulip Karl Palmskog (May 22 2022 at 21:42):

make clean can only clean out .vo files that are listed in _CoqProject

view this post on Zulip Karl Palmskog (May 22 2022 at 21:42):

you may have some other .vo files laying around from before

view this post on Zulip Franklin Pezzuti Dyer (May 22 2022 at 21:43):

I checked for other .vo files manually after running make clean

view this post on Zulip Franklin Pezzuti Dyer (May 22 2022 at 21:43):

all I had left in that folder were testFile1.v and testFile2.v

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Karl Palmskog (May 22 2022 at 21:45):

for example, you could try VsCode+VsCoq

view this post on Zulip 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

view this post on Zulip Karl Palmskog (May 22 2022 at 21:46):

yeah, the two may actually be different executables?

view this post on Zulip Karl Palmskog (May 22 2022 at 21:46):

I always trust the command line more than buttons

view this post on Zulip Franklin Pezzuti Dyer (May 22 2022 at 21:46):

yup. that explains it

view this post on Zulip Franklin Pezzuti Dyer (May 22 2022 at 21:46):

Hahaha fair

view this post on Zulip 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:

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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)


Last updated: Feb 01 2023 at 13:03 UTC