The Coq mailing list

[Donald Leung <i.donaldl AT me.com>]

Dear Théo,

Many thanks for your suggestions and advice (and for filing the bug report!) 
- I used the command line to generate the Makefile from _CoqProject before 
running make on CoqIDE as suggested and got consistent results between the 
make output and the interactive mode.

Cheers,
Donald

> Théo Zimmermann 
> <theo.zimmi AT gmail.com>
>  於 2019年9月6日 01:06 寫道：
> 
> 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