Bug#508468: ITP: ssreflect -- small scale reflection extension for the Coq proof assistant

To: Enrico Tassi <gareuselesinge@debian.org>, 508468@bugs.debian.org
Subject: Bug#508468: ITP: ssreflect -- small scale reflection extension for the Coq proof assistant
From: Stéphane Glondu <steph@glondu.net>
Date: Thu, 11 Dec 2008 23:04:59 +0100
Message-id: <[🔎] 49418E8B.8050707@glondu.net>
Reply-to: Stéphane Glondu <steph@glondu.net>, 508468@bugs.debian.org
In-reply-to: <[🔎] 20081211203750.GA19425@garfield>
References: <[🔎] 20081211145949.10001.8898.reportbug@nickel.pps.jussieu.fr> <[🔎] 20081211203750.GA19425@garfield>

Enrico Tassi wrote:
> I'm interested in that software, but I'm a bit worried on how the
> package could be done. Last time I used it, it was necessary to generate
> a new coq toplevel... Is it now possible to load it on the fly?

It will be with the combination Coq 8.2 / OCaml 3.11. Some people in the
Coq development team are currently working on it. The basic idea is that
the ML part of ssreflect will be compiled into a plugin (.cmxs) that
will be dynamically loaded by Coq when needed.

Cheers,

-- 
Stéphane Glondu

Reply to:

References:
- Bug#508468: ITP: ssreflect -- small scale reflection extension for the Coq proof assistant
  - From: Stephane Glondu <steph@glondu.net>
- Bug#508468: ITP: ssreflect -- small scale reflection extension for the Coq proof assistant
  - From: Enrico Tassi <gareuselesinge@debian.org>

Prev by Date: Bug#508511: ITP: maven-debian-helper -- Helper tools for building Debian packages with Maven
Next by Date: Bug#508512: RFP: GSmartControl-- a GUI for smartmontools
Previous by thread: Bug#508468: ITP: ssreflect -- small scale reflection extension for the Coq proof assistant
Next by thread: Bug#508468: ITP: ssreflect -- small scale reflection extension for the Coq proof assistant
Index(es):
- Date
- Thread