alectryon
alectryon copied to clipboard
--coqc-arg appears to not be passed as expected
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.
It was kindly pointed out to me by Li-yao that I get the correct behaviour if I pass --sertop-arg=--no_prelude
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.
Yes, that is fair enough! I'd be happy to try to improve the situation when I get the chance if you are interested?
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.