The Coq mailing list

[Marcus Ramos <marcus.ramos AT univasf.edu.br>]

Well, almost...

When I execute "make" it works fine, all files are compiled without errors etc. However, when I try to run interactively one of these files in "coqide" I get an error message. For example, consider file Operations_type_3.v:

Require Import Ascii.

Require Import String.

Require Import NPeano.

Require Import Symbols.

Require Import Strings.

Require Import Grammars.

When I try to execute line 4, "Require Import Symbols", I get the message:

Error: The file C:\Users\Marcus Ramos\Documents\UFPE\CIn\Doutorado\Tese\_current\Sources/Symbols.vo contains library

Current.Symbols and not library Symbols

If I change it to "Require Import Current.Symbols" then the message becomes:

Error: Cannot find library Current.Symbols in loadpath

What am I missing here? Do I have to add an "Add LoadPath" line anywhere? Why "make" works and "coqide" not, with the same files?

Thanks,

Marcus.

2013/11/8 Marcus Ramos <marcus.ramos AT univasf.edu.br>

Hi Pierre,

Thanks a lot for the comments, now everything works fine here!

Regards,

Marcus.

2013/11/8 Pierre Boutillier <pierre.boutillier AT pps.univ-paris-diderot.fr>

Hi Marcus,
have you got a working version of "make" in loadpath ?
- no, we are dead :-(
- yes,
create a text file  C:\Users\Marcus
Ramos\Documents\UFPE\CIn\Doutorado\Tese\Current\_CoqProject

that contains
--8<----
-R . Current # to say that this (".") physical folder contains the
logical folder Current
Sources/Ascii.v #aie I just realize the trouble with \ vs / under
windows fill a bug if necessary
Sources/String.v
Sources/NPeano.v
Strings.v
Symbols.v
#any other file of your development
#syntax of this file is documented by "coq_makefile -h"
--8<----

save it close it start coqide with the file Symbols.v

in the preference pane (menubar/edit/preferences)
- custom "Project" part by saying that
* default name for project file is _ProjectFile
* project file options are appened to argument (this way when you'll
open one of the file listed in the _CoqProject file "-R . Current" as
any other option listed in the file will be automatically added to the
underlying coqtop)

(* - custom "External" part by saying
coqmakefile coq_makefile -o makefile -f _CoqProject *)


One for all do "coq_makefile -o makefile -f _CoqProject" in the folder
C:\Users\Marcus Ramos\Documents\UFPE\CIn\Doutorado\Tese\Current\ (now
one each time you edit _CoqProject (to add a file or change options) the
makefile will be automatically autoregenerated)

(MenuBar/Compile/make makefile should work in theory but I'm pretty sure
it won't in practice)

After that each C:\Users\Marcus
Ramos\Documents\UFPE\CIn\Doutorado\Tese\Current\time you need to update
the vo files do make in the folder (MenuBar/Compile/Make is done on that
purpose but I'm pretty sure it won't work because the "underlying shell"
won't be in the good directory)

Pierre B.

On 08/11/2013 16:42, Adam Chlipala wrote:
> On 11/08/2013 10:03 AM, Marcus Ramos wrote:

>> Thanks Adam, but I still can愒 make it. I惻l try to be more specific then:

>>
>> I have a file name "Automata.v" which is located at "C:\Users\Marcus
>> Ramos\Documents\UFPE\CIn\Doutorado\Tese\Current\Sources". This file
>> starts with the following lines:
>>
>> (*--------------------*)
>> Require Import Ascii.
>> Require Import String.
>> Require Import NPeano.
>>
>> Add LoadPath "C:\Users\Marcus
>> Ramos\Documents\UFPE\CIn\Doutorado\Tese\Current" as Current.
>>
>
> I recommend never using "Add LoadPath."  Essentially I'm suggesting
> ignoring source file management commands not described in that chapter
> of CPDT.  This may be an unsatisfying answer from the standpoint of
> particular questions you have about those other commands, but I think it
> sets you on the best practical path.
>
>> When I execute "coqdep *.v" at Sources, I get the messages (besides
>> others):
>
> I suggest never running "coqdep" directly.  I've never done it myself,
> so it's not just that I'm trying to discourage you from using an
> "advanced" feature until you've learned more. ;)  coq_makefile
> encapsulates the important features nicely.