Karl Palmskog (Jun 10 2020 at 17:39): 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...
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
Emilio Jesús Gallego Arias (Jun 10 2020 at 19:55):There's also MMT , I dunno how OMDoc / MMT are used in practice
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.
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
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.
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)
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.
Théo Zimmermann (Jun 11 2020 at 09:40):OK, good to know
Last updated: Oct 13 2024 at 01:02 UTC