New Ticket     Tickets     Wiki     Browse Source     Timeline     Roadmap     Ticket Reports     Search

Ticket #22255 (new submission)

Opened 5 years ago

Last modified 3 days ago

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

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

Change History

Changed 5 years ago by kiyoshi.coquser@…

comment:1 Changed 5 years ago by jmr@…

  • Keywords ssreflect coq removed
  • Version 1.8.1 deleted
  • Type changed from request to submission

comment:2 Changed 5 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 5 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 5 years ago by jobr@…

  • Cc jobr@… added

Cc Me!

comment:5 Changed 4 years ago by jmr@…

  • Port set to ssreflect

comment:6 Changed 3 days ago by mathsmac@…

  • Cc mathsmac@… added

Cc Me!

Note: See TracTickets for help on using tickets.