coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Ian Zimmerman <itz AT very.loosely.org>
- To: Coq-Club Mailinglist <coq-club AT inria.fr>
- Subject: [Coq-Club] Why does coq_makefile impose -q option?
- Date: Sat, 12 Oct 2019 13:55:58 -0700
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=itz AT very.loosely.org; spf=Pass smtp.mailfrom=itz AT very.loosely.org; spf=Pass smtp.helo=postmaster AT very.loosely.org
- Ironport-phdr: 9a23:2nJ2Mhao9W3kafOmG6LNlEj/LSx+4OfEezUN459isYplN5qZr8q/bnLW6fgltlLVR4KTs6sC17ON9f6/EjVdvN6oizMrSNR0TRgLiMEbzUQLIfWuLgnFFsPsdDEwB89YVVVorDmROElRH9viNRWJ+iXhpTEdFQ/iOgVrO+/7BpDdj9it1+C15pbffxhEiCCybL9vIhi6twTcu8sZjYd/Kqs8ygbCr2dVdehR2W5mP0+YkQzm5se38p5j8iBQtOwk+sVdT6j0fLk2QKJBAjg+PG87+MPktR/YTQuS/XQcSXkZkgBJAwfe8h73WIr6vzbguep83CmaOtD2TawxVD+/4apnVAPkhSEaPDMi7mrZltJ/g75aoBK5phxw3YjUYJ2ONPFjeq/RZM4WSXZdUspUUSFOBZ6yb5YUD+oZI+lXs5X9qVUJrRu7HwasBeXvwSJMinL52aA21uIsGhzE0gM9BdIDqHraotXrOqkPUu66w7XHwijNYP5NxTfx9JLFfgw9rfyWQ759d9fax0k1FwPCi1WdsY/rMCmT1u8QsGeb7u9gVeexhG49rgF+uD6vzdorh4nImoIUy0vJ9Ttnz4YvJdy0Ukp7YdmjEJtLqS6aM4t3TtklQ2FytyY307sLsoO1cigNzZQo3R/fa/qffoiN5RLjU+GRLS1ki3JifbKygQu5/0u4yuDkS8W50lhHojBbntTMtn0BzQLf5tWHR/dn/0qs3S6D2gHR5+1ePEw5l6XWJ4Q/zrM+mJcfq1rPEjL0lUjwkaSYbF8r+vKy5OTierjmpoGTN4tzigzmLKQhhNa/AOQiPggKWGib/v+826Pn/Uz5WrlKiec2kqbBvJDbI8QUuLK5DhdI3osh5RuzFSmq3dQYkHUdMl5JZRKKg5LoNlzKOPz4CO2wg1WokDdl3fDGObjhD43MLnjfkbbsZqh95FBGyAsz19xf45VUCrYaIP3tXk/wtMbUDhgjMwy72+rnEsly1psCWWKTBa+UKL/dsViR5u42P+aMYJIVty3mJvg+5//uiGc5lkUHcamo25sXcnG4Ee58L0WXe3q/yusGREwNp08VSPHgwHiLUDpSYXm2XrkgrmUwD5vjBoPeTKishqaA1WG1BMsFSHpBDwWtGHGgRYSBXvoWbSuUaptgji4sS7W7Wskl0ha1uQvrjb19IbyHqWUjqZv/2Y0ttKXonhYo+GkxUp3EjjO9Clpsl2ZNfAcYmaBypUskmgWd3LJpxfhfEsde4+IPVR01Z8eFk75KTuvqUweERe+nDU68S4z2Uy88VMN3x9gJeEt5CpOllB+Rh3P7UY9QrKSCAdkPyoyZ2nHwI8hnzHOfhPs/gkM3BM9IMnargr858BLcVdfE
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?
--
Please don't Cc: me privately on mailing lists and Usenet,
if you also post the followup to the list or newsgroup.
To reply privately _only_ on Usenet and on broken lists
which rewrite From, fetch the TXT record for no-use.mooo.com.
- [Coq-Club] Why does coq_makefile impose -q option?, Ian Zimmerman, 10/12/2019
- Re: [Coq-Club] Why does coq_makefile impose -q option?, Gaëtan Gilbert, 10/12/2019
- Re: [Coq-Club] Why does coq_makefile impose -q option?, Ian Zimmerman, 10/26/2019
- Re: [Coq-Club] Why does coq_makefile impose -q option?, Jason Gross, 10/26/2019
- Re: [Coq-Club] Why does coq_makefile impose -q option?, Ian Zimmerman, 10/26/2019
- Re: [Coq-Club] Why does coq_makefile impose -q option?, Jason Gross, 10/26/2019
- Re: [Coq-Club] Why does coq_makefile impose -q option?, Ian Zimmerman, 10/26/2019
- Re: [Coq-Club] Why does coq_makefile impose -q option?, Jason Gross, 10/26/2019
- Re: [Coq-Club] Why does coq_makefile impose -q option?, Ian Zimmerman, 10/26/2019
- Re: [Coq-Club] Why does coq_makefile impose -q option?, Jason Gross, 10/26/2019
- Re: [Coq-Club] Why does coq_makefile impose -q option?, Ian Zimmerman, 10/26/2019
- Re: [Coq-Club] Why does coq_makefile impose -q option?, Jason Gross, 10/26/2019
- Re: [Coq-Club] Why does coq_makefile impose -q option?, Ian Zimmerman, 10/26/2019
- Re: [Coq-Club] Why does coq_makefile impose -q option?, Gaëtan Gilbert, 10/12/2019
Archive powered by MHonArc 2.6.18.