Skip to Content.
Sympa Menu

coq-club - [Coq-Club] More difficulties with Software Foundations in 8.5

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] More difficulties with Software Foundations in 8.5


Chronological Thread 
  • From: Mitchell Wand <wand AT ccs.neu.edu>
  • To: coq-club AT inria.fr
  • Cc: Benjamin Pierce <bcpierce AT cis.upenn.edu>
  • Subject: [Coq-Club] More difficulties with Software Foundations in 8.5
  • Date: Fri, 29 Jan 2016 14:44:05 -0500
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=mwand1 AT gmail.com; spf=Pass smtp.mailfrom=mwand1 AT gmail.com; spf=None smtp.helo=postmaster AT mail-qk0-f182.google.com
  • Ironport-phdr: 9a23:+Jc8GRc2Sb2zA6smIPbmplrFlGMj4u6mDksu8pMizoh2WeGdxc6/Yx7h7PlgxGXEQZ/co6odzbGG7Oa4BydZuMvJmUtBWaIPfidNsd8RkQ0kDZzNImzAB9muURYHGt9fXkRu5XCxPBsdMs//Y1rPvi/6tmZKSV3BPAZ4bt74BpTVx5zukbvipNuLPU4R3Wf1SIgxBSv1hD2ZjtMRj4pmJ/R54TryiVwMRd5rw3h1L0mYhRf265T41pdi9yNNp6BprJYYAu3SNp41Rr1ADTkgL3t9pIiy7UGCHkOz4S4XVXxTmR5VCSDE6gv7V9H/qHjUrO14jQybIcb2QLQwEQur6asjHADhjisvPDUitmfal4p9gL8N80HpnAB234OBONLdD/F5ZK6IOIpCHWc=
I'm trying to relearn Coq by going through SF version 3.2 (January 2015).

1. make failed at Poly.v .  I added "Set Asymmetric Patterns", which fixed this.
2. make failed again at MoreLogic.v, with the message

coqc  -q  -I .    MoreLogic
File ".\MoreLogic.v", line 3, characters 15-21:
Syntax error: [constr:global] expected after [export_token] (in [vernac:gallina_ext]).
Makefile:202: recipe for target 'MoreLogic.vo' failed
make: *** [MoreLogic.vo] Error 1

The file starts with Require Export "Prop".

I tried removing the quotation marks, and got the following:

$ make
coqdep -c -slash -I .  "MoreLogic.v" > "MoreLogic.v.d" || ( RV=$?; rm -f "MoreLogic.v.d"; exit ${RV} )
warning: option -slash has no effect and is deprecated.
*** Warning: in file MoreLogic.v, library Prop is required and has not been found in the loadpath!
*** Warning: in file MoreLogic.v, library Prop is required and has not been found in the loadpath!
coqc  -q  -I .    MoreLogic
File ".\MoreLogic.v", line 3, characters 15-19:
Syntax error: [constr:global] expected after [export_token] (in [vernac:gallina_ext]).
Makefile:202: recipe for target 'MoreLogic.vo' failed
make: *** [MoreLogic.vo] Error 1

This despite

$ ls Prop*
Prop.glob  Prop.html  Prop.v  Prop.v.d  Prop.vo

How can I fix this?

More generally, is there an up-to-date version of SF that runs out of the box in 8.5 ?

--Mitch




Archive powered by MHonArc 2.6.18.

Top of Page