no message

reviews_v2.txt

+Dear authors,
+
+thanks for your careful response and corrections. I think the work is
+interesting and I recommend publication.
+
+After reading the corrected version, I am still a bit worried with
+regards to the placement of the work in the broader ITP context.
+
+IMO, a key goal of a paper like this is not only to present a particular
+export / data choice, but to help the reader understand why these
+choices were made, and how they do compare to other approaches.
+
+IMVHO designing a data format seems quite a bit of an art, and many
+subtle details tend to become important once the format is used, usually
+in ways that were not anticipated.
+
+I don't think the lack of validation for the export is a major flaw, as
+the accomplishment of the export is an interesting experiment worth
+sharing. But as noted, it goes a very different route.
+
+It is thus important to detail the concrete placement of this particular
+export technology w.r.t. approaches used in other systems, where the
+data export has been motivated from the start by concrete, non-trivial
+uses cases.
+
+For example, Coq has enjoyed machine-friendly export of meta-data for a
+while, in the form of SerAPI, and several non-trivial applications have
+been developed with it [4,5,6].
+
+While there are significant differences between the approaches there, it
+should be noted that these have been validated with sizable developments
+such as the Mathematical Components library or CompCert.
+
+Usually, such approaches do rely on on-demand export of data [but not in
+all cases], and different representation trade-offs. Export on the Coq
+side is faithful and further transformations happen on the application
+side, but the approach tends to be quite low-overhead.
+
+There also is a growing body of work that is exporting proof information
+from Coq, such as [1,2] (and quite a few ongoing projects) for ML use.
+
+While MMT is a more generic format, it seems still open how well it will
+perform for example in ML applications. IMO, the reader should be aware
+of that different approaches as to be able to properly judge the
+strengths and weaknesses of each approach by themselves.
+
+Again, differences on the approaches are IMO non-trivial, as in these
+cases the export format is quite driven by the use cases, but to the
+best of my knowledge, use of the Coq exported data in Machine Learning
+applications has provided a large amount of feedback that have
+influenced quite a few aspects of the export design.
+
+I think that section 6.3 should reference a very relevant line of work [7].
+
+[1] Generating Correctness Proofs with Neural Networks
+    https://arxiv.org/abs/1907.07794
+
+[2] Learning to Prove Theorems via Interacting with Proof Assistants
+    https://arxiv.org/abs/1905.09381
+
+[3] Context-aware Generation of Proof Scripts for Theorem Proving
+    https://easychair.org/publications/preprint/sZBH
+
+[4] Pengyu Nie, Karl Palmskog, Junyi Jessy Li, and Milos Gligoric
+    Learning to Format Coq Code Using Language Models
+    The Coq Workshop
+
+[5] Pengyu Nie, Karl Palmskog, Junyi Jessy Li, and Milos Gligoric
+    Deep Generation of Coq Lemma Names Using Elaborated Terms
+    International Joint Conference on Automated Reasoning
+    (IJCAR 2020), to appear, Paris, France, 2020.
+
+[6] Ahmet Celik, Karl Palmskog, Marinela Parovic, Emilio Jesús Gallego Arias, and Milos Gligoric
+    Mutation Analysis for Coq
+    International Conference on Automated Software Engineering
+    (ASE 2019), 539-551, San Diego, CA, USA, November 2019.
+
+[7] Karl Palmskog, Ahmet Celik, and Milos Gligoric
+    piCoq: Parallel Regression Proving for Large-Scale Verification Projects
+    International Symposium on Software Testing and Analysis
+    (ISSTA 2018), 344-355, Amsterdam, The Netherlands, July 2018.