coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: "Soegtrop, Michael" <michael.soegtrop AT intel.com>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Cc: Benjamin Pierce <bcpierce AT cis.upenn.edu>
Subject: RE: [Coq-Club] More difficulties with Software Foundations in 8.5
Date: Mon, 1 Feb 2016 09:30:44 +0000
Accept-language: de-DE, en-US
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=michael.soegtrop AT intel.com; spf=Pass smtp.mailfrom=michael.soegtrop AT intel.com; spf=None smtp.helo=postmaster AT mga01.intel.com
Ironport-phdr: 9a23:I92vHhKsetvivy70cdmcpTZWNBhigK39O0sv0rFitYgUI/nxwZ3uMQTl6Ol3ixeRBMOAu60C07ud6fC4EUU7or+/81k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i760zceF13FOBZvIaytQ8iJ35vxj7H5oc2LKyxzxxODIppKZC2sqgvQssREyaBDEY0WjiXzn31TZu5NznlpL1/A1zz158O34YIxu38I46Fp34d6XK77Z6U1S6BDRHRjajhtpZ6jiR6WBwCI/z4XVngcuhtOGQnMqh/gFN+luSzj8+F5xSOyPMvsTLlyVy70vIlxTxq9whwAOjEl6mbPzoRVjalbqR+l7VQrxo/fYIiYMLxlea7SYckdXUJAWNpcU2pKBYbqPNhHNPYIIesN99q1nFAJtxbrQFD0XO4=

Dear Mitchell,

just addressing the problem you have: In 8.5 it is no longer possible to have a file named Prop, because Prop is a reserved word. It works if you just rename the file and its references.

Best regards,

Michael

From: mwand1 AT gmail.com [mailto:mwand1 AT gmail.com] On Behalf Of Mitchell Wand
Sent: Friday, January 29, 2016 8:44 PM
To: coq-club AT inria.fr
Cc: Benjamin Pierce
Subject: [Coq-Club] More difficulties with Software Foundations in 8.5

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!

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

Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928

RE: [Coq-Club] More difficulties with Software Foundations in 8.5, Soegtrop, Michael, 02/01/2016