Opened 15 years ago

Last modified 10 years ago

#22255 new submission

New port: ssreflect

Reported by: kiyoshi.coquser@… Owned by: macports-tickets@…
Priority: Normal Milestone:
Component: ports Version:
Keywords: Cc: jobr@…, mathsmac@…
Port: ssreflect

Description

Please add ssreflect to macports.

Ssreflect is a small scale reflection extension for the coq system.

​http://www.msr-inria.inria.fr/Projects/math-components/

NOTE: To install ssreflect, coq should be fixed by #22254.

Attachments (1)

Portfile​ (2.0 KB) - added by kiyoshi.coquser@… 15 years ago.

Download all attachments as: .zip

Change History (7)

Changed 15 years ago by kiyoshi.coquser@…

Attachment: Portfile​ added

comment:1 Changed 15 years ago by jmroot (Joshua Root)

Keywords: ssreflect coq removed
Type: request → submission
Version: 1.8.1

comment:2 Changed 15 years ago by kiyoshi.coquser@…

Ticket #22254 is fixed.

So there is no reason to defer the addition of ssreflect to macports, now.

comment:3 Changed 15 years ago by jobr@…

I get the following error after installing with the attached Portfile on a freshly-compiled Coq 8.2pl1. 

Coq < Require Import ssreflect.
Error: The file /opt/local/lib/coq/user-contrib/theories/ssreflect.vo contains library
ssreflect and not library theories.ssreflect

comment:4 Changed 15 years ago by jobr@…

Cc: jobr@… added

Cc Me!

comment:5 Changed 14 years ago by jmroot (Joshua Root)

Port: ssreflect added

comment:6 Changed 10 years ago by mathsmac@…

Cc: mathsmac@… added

Cc Me!

Note: See TracTickets for help on using tickets.