> 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
On Mon, 9 Apr 2012, Edward Z. Yang wrote:
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 yx
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
On Sun, 8 Apr 2012, Edward Z. Yang wrote:
I took a look at the YXML encoding for Isabelle, and I was surprised by
how simple the ADT was. To compare, here is Coq's base term type;
and it doesn't include all of the extra types referred to from it:
type ('constr, 'types) kind_of_term =
|
On Sun, 08 Apr 2012 14:24:45 -0400, "Edward Z. Yang" wrote:
> 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 us
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
On Fri, 6 Apr 2012, Edward Z. Yang wrote:
Anyway, what is your front-end technology (also the programming
language platform for that)? Why are you using PGIP anyway?
Uh, it's a bit of an unholy soup of all the languages (right now we're
doing Haskell and Urweb, but I'm very happy to drop/add
On Fri, 6 Apr 2012, Edward Z. Yang wrote:
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 obsol
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, "Edward Z. Yang" wrote:
> > Yes, this
On Fri, 06 Apr 2012 12:00:39 -0400, "Edward Z. Yang" wrote:
> Yes, this is another approach that we have considered. Actually, in this case
> I would have wanted to cut out the middleman, lib-ified Coq and just run 'open
> Coq' and directly do this (this may be worth doing anyway, independent of
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
> 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
On Fri, 6 Apr 2012, Edward Z. Yang wrote:
I'm actually building a domain-specific frontend for Coq, and I didn't
feel like reimplementing all of ProofGeneral's parsing hacks! It's not
much: it's going to be a pedagogical theorem prover for first order
logic, but the idea is to closely support
On Fri, 6 Apr 2012, David Aspinall wrote:
Interesting that you're trying this! Although I should warn that we
haven't been actively developing the PGIP infrastructure for a while:
which interface are you hoping to use it with?
In fact, I recently considering asking if it is now time to remov
Sounds interesting! Good luck and let us know if we can help again.
- D.
On 6 Apr 2012, at 09:04, Edward Z. Yang wrote:
> Hello David,
>
> I'm actually building a domain-specific frontend for Coq, and I didn't
> feel like reimplementing all of ProofGeneral's parsing hacks! It's
> not much: i
Hello David,
I'm actually building a domain-specific frontend for Coq, and I didn't
feel like reimplementing all of ProofGeneral's parsing hacks! It's
not much: it's going to be a pedagogical theorem prover for first
order logic, but the idea is to closely support different deduction
styles (e.g.
Hello Edward
Interesting that you're trying this! Although I should warn that we haven't
been actively developing the PGIP infrastructure for a while: which interface
are you hoping to use it with?
Anyway, you should have no problem with multiple in PGIP. You
need to set the fatality attrib
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
18 matches
Mail list logo
