New Ticket     Tickets     Wiki     Browse Source     Timeline     Roadmap     Ticket Reports     Search

Ticket #22255 (new submission)

Opened 4 years ago

Last modified 2 years ago

New port: ssreflect

Reported by: kiyoshi.coquser@… Owned by: macports-tickets@…
Priority: Normal Milestone:
Component: ports Version:
Keywords: Cc: jobr@…
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@… 4 years ago.

Change History

Changed 4 years ago by kiyoshi.coquser@…

comment:1 Changed 4 years ago by jmr@…

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

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

  • Cc jobr@… added

Cc Me!

comment:5 Changed 2 years ago by jmr@…

  • Port set to ssreflect
Note: See TracTickets for help on using tickets.