Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Running make in CoqIDE 8.9.1 with _CoqProject file works but Forward one command fails

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Running make in CoqIDE 8.9.1 with _CoqProject file works but Forward one command fails


Chronological Thread 
  • From: Théo Zimmermann <theo.zimmi AT gmail.com>
  • To: Coq Club <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] Running make in CoqIDE 8.9.1 with _CoqProject file works but Forward one command fails
  • Date: Thu, 5 Sep 2019 19:06:21 +0200
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=theo.zimmi AT gmail.com; spf=Pass smtp.mailfrom=theo.zimmi AT gmail.com; spf=None smtp.helo=postmaster AT mail-ua1-f65.google.com
  • Ironport-phdr: 9a23:6MRzBRb7PfhN95MJRsGzcE7/LSx+4OfEezUN459isYplN5qZr8y8bnLW6fgltlLVR4KTs6sC17OM9fm/BidRuN6oizMrSNR0TRgLiMEbzUQLIfWuLgnFFsPsdDEwB89YVVVorDmROElRH9viNRWJ+iXhpTEdFQ/iOgVrO+/7BpDdj9it1+C15pbffxhEiCCybL9vMhm6txjdu8sUjIdtLqs91wbCr2dVdehR2W5mP0+YkQzm5se38p5j8iBQtOwk+sVdT6j0fLk2QKJBAjg+PG87+MPktR/YTQuS/XQcSXkZkgBJAwfe8h73WIr6vzbguep83CmaOtD2TawxVD+/4apnVAPkhSEaPDMi7mrZltJ/g75aoBK5phxw3YjUYJ2ONPFjeq/RZM4WSXZdUspUUSFKH4GyYJYVD+cZMulYoYvyqVsAoxW9GAeiGv/gxDBTi3/qxK03yfgtHR3a0AEiGd8FrXTarM/yNKcXSe270qnIyi/Eb/xO2jj96Y3IchU/rvGWWLJ/a8zRyU8yHA7CklWQqZLqPzSP2uUMsmib6u9gVeO0hm4orgF+uDmvxsM2hobVgYIVz0nJ+CNky4g7It24TVR0Yd+iEJZIuCGaNpd2QsM/Q25zoio11roGuZu9cSMXy5on3wbSZ+Kbf4WM+B7uV+acLS1miH57Zr6znRe//Eimx+bhTMe7ykxKoTBAktTUtnACyRjT6s+fR/t45Eih2DKP2xnO6u5ePEw4jKTbJp8hz7IqmZoTtkPDHiDymErolqOZakIk+u2w5+TmZLXpuIOcOpdqhg3iNqkigM+yDOQiPgQQQWSX5/6w2bzj8EHhRbVFlPw2kq3XsJDAIsQbo7a0AxNV0ok97BazFTan0NUdnXkCLVJIYx2Hj43zNFHPJPD0F+uwg1OpkDtz3fDJIqXhAonRLnjEiLruYbF961dFxAUvydBf+olbB6oaIPPzX0/xrMbXAgU4Mwyy2ebnCc9y2pkQWWKVUeelN/b5tkbAzeYyKaHYb4gM/T35NvIN5vj0jHZ/l0VLLoez2p5CVHA5GcNUIkCcbGDpi9EHWTMWvgc5Cv7rjViDeTFWbne2Gak742doW8qdEY7fS9X10/S61yChE8gTPzgeUwHeITLTb4yBHsw0RmeXK85lnCYDUOH4GYAk3BCq8gT9zug+d7eGymgjrZvmkeNNyajTmBU1r2EmCs2c1ySQRjgxkD1VATAx2697rAp2zVLRifEk0cwdLsRa4rZyail/LYTVlrUoBNX7WwaHddCMGg6r

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



Archive powered by MHonArc 2.6.18.

Top of Page