The Coq mailing list

[Pierre Courtieu <Pierre.Courtieu AT cnam.fr>]

I suppose that Int, gen, and the current directory are actually 3 different coq libraries. If this is not the case you need to tell us a bit more. If this is the case then they should not share the same _CoqProject file.

1) Go inside Int directory and type make, if it went well, then do "make install".

3) do the same in directory gen

now coq knows about Int and gen without any -Q option. Write your _CoqProject by mentioning only your files. By default "make install" copies .vo files into <coq_directory>/user-contrib/<libdirectoryname>, which is searched by coq by default.

Hope this helps,

Pierre

Le lun. 27 avr. 2020 à 16:50, Jeremy Dawson <Jeremy.Dawson AT anu.edu.au> a écrit :

Sorry, I don't understand what you are getting at.  What do you mean by
make *and make install* tense-logic-in-Coq
ie what do I type and in what directory?
What is "make install" meant to do?

Thanks

Jeremy


On 4/28/20 12:01 AM, Pierre Courtieu wrote:
> Hi
>
> These warnings mean that your current configuration does not allow to do
> "make install" due to the lack of a main root directory. coq_makefile
> does not support to install several libraries at once. However I think
> you should be able to built your project without problems.
>
> That said if you make *and make install* tense-logic-in-Coq you could
> just remove it completely from you _CoqProject file, use it in your
> development and have a working "make install".
>
> Hope this helps,
> P
>
>
> Le lun. 27 avr. 2020 à 13:39, Jeremy Dawson <Jeremy.Dawson AT anu.edu.au
> <mailto:Jeremy.Dawson AT anu.edu.au>> a écrit :
>
>     Hi,
>
>     Thanks - but this won't work because it would mean changing dd_fc.v
>     and all the files in that directory, which is part of other people's
>     work as well
>
>     So I tried some alternatives like
>     -Q ../lnt/tense-logic-in-Coq/
>     or
>     -Q ../lnt/tense-logic-in-Coq/ .
>
>     All of these, including your suggested
>     -Q ../lnt/tense-logic-in-Coq/ TL
>
>     gave a bunch or warnings, eg
>
>     -Q ../lnt/tense-logic-in-Coq/ TL
>     gives
>     Warning: ../lnt/tense-logic-in-Coq/ (used in -R or -Q) is not a
>     subdirectory of the current directory
>
>     Warning: no common logical root
>     Warning: in such case INSTALLDEFAULTROOT must be defined
>     Warning: the install-doc target is going to install files
>     Warning: in orphan_TL_Top
>
>     I don't understand any of these, except the first (and I don't know
>     what
>     I should do about that), and I can't find any explanation of these in
>     the documentation.
>
>     What do they all mean?
>
>     Thanks
>
>     Jeremy
>
>
>     On 27/4/20 12:26 am, Gaëtan Gilbert wrote:
>      > Indeed -I is for ocaml files (for plugins)
>      >
>      > Gaëtan Gilbert
>      >
>      > On 26/04/2020 16:23, Dan Frumin wrote:
>      >> Hi Jeremy,
>      >>
>      >> I don't know why -I doesn't work, but I think using -Q does the
>     trick
>      >> (at least with my version of Coq): I replaced
>      >>
>      >>      -I ../lnt/tense-logic-in-Coq/
>      >>
>      >> with
>      >>      -Q ../lnt/tense-logic-in-Coq/ TL
>      >>
>      >> and then in dd_fc.v used `Require Import TL.genT`
>      >>
>      >>
>      >>
>      >> Best,
>      >> Dan
>      >>
>      >>
>      >> On 26-04-2020 16:09, Jeremy Dawson wrote:
>      >>>
>      >>> Hi,
>      >>>
>      >>> I've constructed a _CoqProject file as follows
>      >>>
>      >>> -I ../lnt/tense-logic-in-Coq/
>      >>> -I ../gen/
>      >>> ../lnt/tense-logic-in-Coq/gen.v
>      >>> ../lnt/tense-logic-in-Coq/genT.v
>      >>> ../lnt/tense-logic-in-Coq/List_lemmasT.v
>      >>> ../lnt/tense-logic-in-Coq/lntT.v
>      >>> ../lnt/tense-logic-in-Coq/swappedT.v
>      >>> ../lnt/tense-logic-in-Coq/ddT.v
>      >>> ../lnt/tense-logic-in-Coq/dd_fc.v
>      >>> ../lnt/tense-logic-in-Coq/lntacsT.v
>      >>> ../gen/rtcT.v
>      >>> ../gen/gstep.v
>      >>> ../gen/gentree.v
>      >>> gen_ext.v
>      >>> k4.v
>      >>> k4_exch.v
>      >>> k4_inv.v
>      >>> k4_ctr.v
>      >>> k4_ca.v
>      >>>
>      >>> I then run
>      >>>   make -f Makefile
>      >>> and get the following messages
>      >>> COQC ../lnt/tense-logic-in-Coq/dd_fc.v
>      >>> File "../lnt/tense-logic-in-Coq/dd_fc.v", line 12, characters
>     15-19:
>      >>> Error: Unable to locate library genT.
>      >>>
>      >>> (in fact the file
>      >>> ../lnt/tense-logic-in-Coq/genT.v
>      >>> exists)
>      >>>
>      >>> What do I need to put in the _CoqProject file to make this work?
>      >>>
>      >>> Thanks
>      >>>
>      >>> Jeremy
>