The Coq mailing list

["Benjamin C. Pierce" <bcpierce AT cis.upenn.edu>]

Hi Mitch,

We’re working now on a version of SF that works with both 8.4 and 8.5.  The change to 8.5 is already done, but the whole thing is going to take a few more weeks to release because we’re doing a bunch of other reorganization and rewriting at the same time.  The new version will be announced here when it’s ready.

    - Benjamin

On Jan 29, 2016, at 2:44 PM, Mitchell Wand <wand AT ccs.neu.edu> wrote:

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