The Coq mailing list

[Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net>]

make COQFLAGS=

Gaëtan Gilbert

On 12/10/2019 22:55, Ian Zimmerman wrote:
> I am trying to enhance my minimal knowledge of coq in the following
> context:
>
> - classical logic
> - ssreflect tactic language
> - unicode symbols
>
> This means that every one of my .v files needs the following boilerplate
> at the beginning:
>
>  From mathcomp Require Import ssreflect ssrfun ssrbool.
> Require Import FunctionalExtensionality.
> Require Import ClassicalEpsilon.
> Require Import PropExtensionality.
> Set Implicit Arguments.
> Unset Strict Implicit.
> Unset Printing Implicit Defensive.
> Require Import Utf8.
>
> So far the only way I've thought of to avoid in fact typing all this is
> to use the "initfile" or "rcfile".  So I added this to my _CoqProject:
>
> -arg -init-file
> -arg ,coqinit
>
> where the contents of ,coqinit are as above.
>
> And I see that after running coq_makefile, make VERBOSE=1 does something
> like:
>
>   matica!41 ssreflect-playground$ make VERBOSE=1
> "coqdep" -dyndep var -f _CoqProject   > ".coqdeps.d" || ( RV=$?; rm -f 
> ".coqdeps.d"; exit $RV )
> make --no-print-directory -f "Makefile" pre-all
> if [ "8.9.1" != "8.9.1" ]; then\
>    echo "W: This Makefile was generated by Coq 8.9.1";\
>    echo "W: while the current Coq version is 8.9.1";\
> fi
> make --no-print-directory -f "Makefile" real-all
> "coqc"   -q  -init-file ,coqinit  -R . Top Group_abstract.v
> File "./Group_abstract.v", line 3, characters 42-45:
> Error: Syntax Error: Lexer: Undefined token
>
> So ... -init-file is getting passed correctly, but it has no effect
> because it is accompanied by -q.  Why does coq_makefile pass -q to coqc,
> and how can I change this behavior?