Ssreflect Users Discussion List

[Bas Spitters <>]

Dear Georges,

1> Your suggestion seems to work. The patch does not seem to be needed anymore.

2> I guess I need OCaml 3.11 to use plugins. A rather wait a while for it to be packaged in all the main distributions.

3> So, this is a nice research question...

Best,

Bas

On Friday 04 September 2009 13:10:46 Georges Gonthier wrote:
>   Hi Bas,
>
>      Welcome to ssreflect! Thanks for your input; here are a few answers:
>
> 1>     I'm afraid I can't accept your identifiers patch, because ssreflect
> DOES use one-letter _x_ identifiers: these are the identifiers that are
> auto-generated by anonymous ? and * intro patterns. It's important to keep
> the user from referring to those, because this significantly improves the
> robustness of scripts (I implemented this feature after getting burned
> because I'd lapsed in my naming discipline). Ssreflect already gives you an
> option to disable the check (use Unset SsrIdents), but it still will warn
> you each time you use them, so this only a partial fix. If (as I'd guess)
> Corn uses _C_ and _X_ for global constants, a better solution would be to
> declare them as proper reserved identifiers, using, say, Notation "'_X_'"
> := Corn_polynomial_variable.
>       If this doesn't cut it then I'd have to refine the SsrIdents option
> to allow disabling the warning... which I'd rather not. For the record, the
> decision to impinge on the user identifier space was forced onto me:
> Ssreflect 1.1 used internal spaces for its reserved identifiers, and I'd
> planned to switch to short comment sequences (e.g. (**)x) to improve
> readback and extraction in for the 1.2 update, but then the Coq devs added
> an internal system check that would have caused random crashes with this
> policy, thus forcing these namespace compatibility conflicts onto me.
>
> 2>     coq_makefile already supports -custom attributes in the Make file it
> uses to create a Makefile: indeed, this is how the ssreflect library is
> compiled. Also if you're able to get a working Ocaml that supports plugins
> you can try Stephane's suggestion (I haven't), but then I'd recommend
> putting the Require line in either a .coqrc file, or in a Coq compile
> option, rather than modifying ssreflect.v.
>
> 3>     I'm afraid that Corn is trying to address exactly the blind spot of
> the ssralg hierarchy. The rationale for ssralg is that either you're
> interested in effective constructions, in which case all you data types
> will ultimately be concrete and most properties of interest will be
> decidable, or you're doing classic maths, in which case everything is
> decidable by assumption. The ssralg interfaces encapsulate fairly cleanly
> the quanta of classicism that  might be needed, so that the rest of the
> libraries can work equally well in either a classic or a concrete
> constructive setting. Unfortunately that leaves out Corn, which is targeted
> at the abstract (intuitionistic) constructive setting.
>
>    Hope this helped, cheers,
>
> Georges
>
> ________________________________
> From: Bas Spitters [mailto:]
> Sent: 04 September 2009 11:07
> To: 
> Subject: Ssreflect and corn
>
> Hello,
>
>
>
> I am adapting corn to use ssreflect.
>
>
>
> It seems that a few changes are needed:
> 1.
> ---
> There are conflicts of notations between Ssreflect and CoRN.
> The Ssreflect toplevel also declares the identifiers of the form _*_ as
> reserved, and CoRN polynomials use identifiers _C_ and _X_. The patch
> Ssreflect.patch modifies ssreflect.ml to allow identifiers for which there
> is a single letter between the underscores. The patch was provided by
> Valentin Blot.
> ---
>
>
>
> 2.
> It would be nice of ssreflect could provide replacements for all the
> standard coq tools. For instance: Add a custom target to the Makefile:
> ----
> bin/ssrcoqide: src/ssreflect.cmx
> $(COQBIN)coqmktop -ide -opt -o "$@" src/ssreflect.cmx
> ----
>
>
>
> 3.
> Finally, a question. The ssreflect algebraic hierarchy seems to be solely
> focussed on decidable structures. Are there any plans or ideas on
> supporting non-decidable structures?
>
>
>
>
>
> Best regards,
>
>
>
> Bas