Stream: Coq devs & plugin devs

Topic: OMDoc theory exporting


view this post on Zulip Karl Palmskog (Jun 10 2020 at 17:39):

I looked a bit at the OMDoc export for Coq (https://kwarc.info/people/frabe/Research/MRS_coq_19.pdf), and now for Isabelle (https://arxiv.org/abs/2005.08884). @Emilio Jesús Gallego Arias have you looked at how OMDoc XML compares to what we produce through SerAPI/sercomp? For example, I would be a bit suprised if it contains lexer tokens...

view this post on Zulip Emilio Jesús Gallego Arias (Jun 10 2020 at 19:54):

Karl Palmskog said:

I looked a bit at the OMDoc export for Coq (https://kwarc.info/people/frabe/Research/MRS_coq_19.pdf), and now for Isabelle (https://arxiv.org/abs/2005.08884). Emilio Jesús Gallego Arias have you looked at how OMDoc XML compares to what we produce through SerAPI/sercomp? For example, I would be a bit suprised if it contains lexer tokens...

I have only a rough idea; but indeed there are several key differences AFAICS. For example, serapi is usually faithful, also it doesn't build a kind of theory definition but is definitively more low-level

view this post on Zulip Emilio Jesús Gallego Arias (Jun 10 2020 at 19:55):

There's also MMT , I dunno how OMDoc / MMT are used in practice

view this post on Zulip Karl Palmskog (Jun 10 2020 at 19:57):

I see. In the Isabelle paper (came out only a few weeks ago) they say things can be connected to the source file by something similar to SerAPI'sloc, although they don't explain it that way.

view this post on Zulip Karl Palmskog (Jun 10 2020 at 19:58):

the main difference on the Coq side might be that the XML exporting plugin is stuck at 8.9 (drawback of not being hooked into Coq), but on the Isabelle side probably Makarius has set up some way to maintain OMDoc export

view this post on Zulip Théo Zimmermann (Jun 11 2020 at 08:46):

XML exporting plugin is stuck at 8.9 (drawback of not being hooked into Coq)

I don't understand what is going on with this. The lack of communication of Claudio with the Coq dev team on this matter and the fact that Logipedia intends to depend on it to do their Coq import worries me.

view this post on Zulip Karl Palmskog (Jun 11 2020 at 09:07):

it's also worth noting that the OMDoc export seems extremely verbose. Our corpus is about 300k .v LOC from 22 projects, and it takes maybe 1.6GB to store it uncompressed (~120MB compressed). Claudio's corpus has 49 projects and takes 17GB when heavily compressed (the compressed archive has more than 1.2 million XML files)

view this post on Zulip Enrico Tassi (Jun 11 2020 at 09:09):

If the logipedia project passes, then I'm supposed to work (with Claudio) at improving the integration with Coq.

view this post on Zulip Théo Zimmermann (Jun 11 2020 at 09:40):

OK, good to know


Last updated: Oct 21 2021 at 21:03 UTC