The Coq mailing list

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

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