Commit c9f0bbb1 authored by Florian Rabe's avatar Florian Rabe

no message

parent c40007d9
# documentation
h# documentation
Articles describing the library export
\ No newline at end of file
......@@ -2,21 +2,19 @@ We have taken care of all minor comments.
We believe the following are the major comments where a response is expected.
Review 1+3 would like to see a clear use of the produced data.
We believe our data is easier to reuse than that provided by Coq itself because a lot of Coq expertise is needed to pull the data out of the Coq kernel.
We have started using the produced data for searching and querying the Coq library. We will mention that as future work.
Our data is also ready for rechecking the Coq library - the bottleneck here is mimicking all the subtleties of Coq's typing rules (as implemented).
Firstly, we believe our data is easier to reuse (e.g., for library analysis, machine learning, rechecking) than that provided by Coq itself because a lot of Coq expertise is needed to pull the data out of the Coq kernel.
Secondly, we have started using the produced data for some applications, specifically searching and querying the Coq library. We will discuss that as future work.
Review 3 calls the comparison to Coqine unfair.
We did not mean to disparage Coqine and will rephrase.
Coqine errs on the side of recheckability even if that means not being applicable to a large portion of the library. Our translation errs on the side of total applicability, which naturally makes rechecking a lot harder.
Coqine errs on the side of recheckability even if that means only covering a small fragment of the Coq library.
Our translation errs on the side of total applicability, which naturally makes rechecking as hard as reimplemeting all the subtleties of Coq's typing rules.
@CSC: Can you say something here?
Review 2 points out the overlap with the paper on the XML export.
> Maybe it would make sense to factor it out in case both papers are published?
If both papers are accepted, we will refactor accordingly.
Reviewer 3 says that the modular structure of the Coq library is less interesting than the one of type classes and canonical structures.
We agree. But exporting that is even harder. So we need the present as a stepping stone towards it.
We agree. But exporting that is even harder. So we need the present translation as a stepping stone towards it.
-------------------------------------------- do not submit below here ---------------------------------
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment