Hello all,
I'm working on partial PGIP support Coq, and one thing that I would like
to support is the case when Coq outputs "warning" messages, of which
there are many but which are nonfatal. I'm wondering what the right
tag for these are. is not correct, because we're only
allowed to have one
In sort of the same vein, in Coq, we have named hypotheses in our
proof contexts which render like:
Hyp0 : Hyp (P x)
Hyp1 : Hyp (P z)
or (P x) (or (forall y : U, P y) False)
I'd like to add some PGML so that it looks something like this:
Hyp0 :
"). The restriction you mention applies to the plain text
> protocol used inside Emacs for real errors, which correspond to PGIP
> .
>
> Hope this helps,
>
> - David
>
> On 6 Apr 2012, at 04:15, Edward Z. Yang wrote:
>
> > Hello all,
> >
> &g
> The "parsing hacks" are hacks as long as there is an attempt to define
> that in a generic protocol. For example, Isabelle/Scala now lets the
> prover do that reliably (either in ML or Scala). I have recently
> discussed with some Coq insiders how to do the same specifically for Coq,
> usin
Excerpts from Makarius's message of Fri Apr 06 06:34:47 -0400 2012:
> More than 4 years of Isabelle/Scala there is sufficient infrastructure to
> make it obsolete, and the "flagship application" of Isabelle/jEdit is
> doing reasonably well.
If PGIP is obsolete I would love to know, then I will n
Cool! (Though, wouldn't it have been easier to write the IRC
bot in OCaml ;-) How do you build coqpy.m4? I'm not sure
what a 'Make' file is.
Edward
Excerpts from Tom Prince's message of Fri Apr 06 18:57:25 -0400 2012:
> On Fri, 06 Apr 2012 12:00:39 -0400, "Edwa
Excerpts from Makarius's message of Sat Apr 07 08:43:57 -0400 2012:
> Cutting out the middleman is a good start. The lib-ified approach sounds
> more like running everything in a single OCaml process, though. The Coq
> guys used to have that for CoqIde, but discontinued it for the forthcoming
Excerpts from Makarius's message of Mon Apr 09 09:50:09 -0400 2012:
> You would have compare that to the datatypes for term and proofterm in
> Isabelle, see src/Pure/term.ML and src/Pure/proofterm.ML, respectively.
Ah, so is the sample term encoding in yxml not representative of
Isabelle? I misun
> Maybe I've misunderstood this as a misunderstanding. The example term
> representation for the YXML library is exactly the Isabelle term datatype.
> But that is really just an example, it is not really useful for the
> problem to connect users to proof checkers.
Oh, I see.
No, it does seem
