--coqc-arg appears to not be passed as expected

[Boarders]

Hi,

This is a really amazing tool, thank you for making it! I may be using it incorrectly, but when I try to invoke it as:

alectryon --frontend coq --coqc-arg=-noinit --coqc-arg=-indices-matter ch1.v

This gives me a long list of warnings. I get the same warnings if I run coqc ch1.v but not if I run coqc -noinit -indices-matter ch1.v. Am I doing something incorrectly here?

Here is a cut down version of the file I am trying this on:

From HoTT Require Import HoTT.

Local Open Scope path_scope.
Local Open Scope equiv_scope.
Local Open Scope fibration_scope.

(*| Exercise 1.1 
 Given functions f : A → B and g : B → C, define their composite g ◦ f : A → C.
Show that we have h ◦ (g ◦ f ) ≡ (h ◦ g) ◦ f . |*)
Definition comp {A B C : Type} (g : B -> C) (f : A -> B) : A -> C :=
  fun x => g (f x).

Theorem comp_assoc : forall {A B C D : Type} (f : A -> B) (g : B -> C) (h : C -> D),
    comp h (comp g f) = comp (comp h g) f.
Proof.
  reflexivity.
Qed.

(*| 
Exercise 1.2. Derive the recursion principle for products recA×B using only the projections, and
verify that the definitional equalities are valid. Do the same for Σ-types. |*)
Definition prod_rec {A B C : Type} (f : A -> (B -> C)) (p : A * B) : C :=
  f (fst p) (snd p).

Theorem prod_comp : forall {A B C : Type} (f : A -> (B -> C)) (a : A) (b : B),
    prod_rec f (a , b) = f a b.
Proof.
  reflexivity.
Qed.

Definition sigma_rec {A B : Type} {P : A -> Type}
           (f : forall (a : A), P a -> B) (p : { a | P a}) : B :=
  f (p .1) (p .2).

Theorem sigma_comp :
  forall {A B : Type} {P : A -> Type}
         (f : forall (a : A), P a -> B) (a : A) (pa : P a),
    sigma_rec f (a ; pa) = f a pa.
Proof.
  reflexivity.
Qed.

[Boarders]

It was kindly pointed out to me by Li-yao that I get the correct behaviour if I pass --sertop-arg=--no_prelude

[cpitclaudel]

Thanks for the report and thanks Li-yao for the solution! I think the bug here is that you didn't get a warning: the coqc-arg flags don't apply unless you use the coqc_time driver.

[Boarders]

Yes, that is fair enough! I'd be happy to try to improve the situation when I get the chance if you are interested?

[cpitclaudel]

That would be lovely! It would be in cli.py, where it maps each argument to the corresponding driver. We'd add a final check that the only arguments that are set are for the selected driver and warn if not.