The Coq mailing list

[Théo Zimmermann <theo.zimmi AT gmail.com>]

Hi Donald,

It seems that you have just found a bug with the "Make makefile" menu
(now reported as https://github.com/coq/coq/issues/10736).
As you can see when it displays a successful result (in the bottom
bar), it has run the command "coq_makefile -o makefile *.v" instead of
using the _CoqProject file in the directory.
Now if instead you used the command-line to run "coq_makefile -f
_CoqProject -o Makefile", then you can use the CoqIDE menu (or the
command-line) to compile, and it will properly work.

By the way, the use of "" as a logical name is discouraged (and you
will get a warning when generating the Makefile). I'd recommend you
put a real logical name, like Foo. However, if you do so, you'll have
to either use -R instead of -Q, or require import "Foo.Preloaded"
instead of "Preloaded".

Théo

Le jeu. 5 sept. 2019 à 13:38, Donald Leung 
<i.donaldl AT me.com>
 a écrit :
>
> Dear coq-clubbers,
>
> I recently noticed an email where Théo Zimmerman suggested the use of a 
> _CoqProject file over using Add LoadPath within a vernacular file (because 
> I’m used to (ab)using Add LoadPath whenever files don’t link up) and 
> decided to look into writing a _CoqProject file for a mini project.
>
> Currently, within a folder on my desktop, I have the following files:
>
> _CoqProject:
>
> ```
> -Q . ""
> Preloaded.v
> Solution.v
> ```
>
> Preloaded.v:
>
> ```coq
> Require Import ZArith List Lia.
> Import Z.
> Open Scope Z_scope.
>
> Fixpoint total (xs : list Z) :=
>   match xs with
>   | nil => 0
>   | x :: xs' => x + total xs'
>   end.
>
> Definition Sub (a xs : list Z) :=
>   exists pre suf, xs = pre ++ a ++ suf.
>
> Definition Max_sub_sum (a xs : list Z) :=
>   Sub a xs /\ (forall b, Sub b xs -> total b <= total a).
>
> Fixpoint max_sub_sum_aux (xs : list Z) : Z * Z :=
>   match xs with
>   | nil => (0, 0)
>   | x :: xs' =>
>       let (p, q) := max_sub_sum_aux xs' in
>         (max 0 (x + p), max (x + p) q)
>   end.
>
> Definition max_sub_sum (xs : list Z) := snd (max_sub_sum_aux xs).
> ```
>
> Solution.v:
>
> ```coq
> Require Import Preloaded ZArith List.
>
> (* Hope this helps *)
> Require Import Lia.
>
> Import Z.
> Open Scope Z_scope.
>
> Theorem max_sub_sum_correct : forall (xs : list Z),
>   exists s, Max_sub_sum s xs /\ total s = max_sub_sum xs.
> Proof.
>   (* FILL IN HERE *)
> Admitted.
>
> Print Assumptions max_sub_sum_correct.
> ```
>
> Using CoqIDE 8.9.1, I noticed that when I run Compile > Make makefile 
> followed by Compile > Make, all the associated files get compiled 
> successfully with the following output:
>
> ```
> Compilation output:
>
> COQDEP VFILES
>
> COQC Preloaded.v
>
> COQC Solution.v
>
> Axioms:
> max_sub_sum_correct : forall xs : list Z,
>                       exists s : list Z,
>                         Max_sub_sum s xs /\ total s = max_sub_sum xs
>
> ```
>
> However, when I try Forward one command on the first line of Solution.v, it 
> fails with the error message “The file 
> /Users/donaldl/Desktop/kata/Preloaded.vo contains library Top.Preloaded and 
> not library Preloaded”. What does that mean and how can I make my files 
> work both using make and interactive stepping?
>
> Cheers,
> Donald