From 787a6e987c29483eb2403c6c982eb675735f6aa4 Mon Sep 17 00:00:00 2001 From: m-iancu <mihnea.iancu88@gmail.com> Date: Thu, 21 Apr 2016 19:27:11 +0200 Subject: [PATCH] updated rebuttals --- mmt-stex/rebuttal.txt | 16 +++---- structural-extensions/rebuttal.txt | 74 +++++++++++++++--------------- 2 files changed, 45 insertions(+), 45 deletions(-) diff --git a/mmt-stex/rebuttal.txt b/mmt-stex/rebuttal.txt index 44fde26..6af8f6c 100644 --- a/mmt-stex/rebuttal.txt +++ b/mmt-stex/rebuttal.txt @@ -7,31 +7,31 @@ little related work (javadoc not literate programming issue) ---------------- Rebuttal ---------------- -Let us start off with clarifying that the paper is intented as a Systems paper. Therefore +Let us start off with clarifying that the paper is intended as a Systems paper. Therefore, related work and theoretical aspects are downplayed. -Even though we focus on MMT and sTeX, our system design scales arbitrary surface languages +Even though we focus on MMT and sTeX, our system design scales to arbitrary surface languages that elaborate into a common base language. Our system implementation is indeed restricted to OMDoc as a base language, but it does scale to arbitrary surface languages. -In general, we believe that the base/surface language dualilty (which is pertinent to many -ITP/MKM/CAS systems) is under-discussed in the community. And we see our system as a +In general, we believe that the base/surface language duality (which is pertinent to many +ITP/MKM/CAS systems) is under-discussed in the community. We see our system as a contribution to this. The access issues reported by Reviewer 2/3 were a GitLab configuration issue that has been since fixed. We acknowledge that the system is hard to install (the LaTeXML dependency is heavy), but the system is intended as part of the MMT/MathHub system, which we distribute -as a docker container as with pre-installed dependencies. Therefore separate installation +as a docker container as with pre-installed dependencies. Therefore separate installation has not been a priority. Reviewer 3 misunderstood our (technically correct, but perhaps ambiguous) remark about literate programming. We are not claiming that javadoc is an instance of literate -programming, but that both are instances of the mixing technique, which is an escaping -mechanism into other langauges. +programming, but rather that both of them are instances of the mixing technique, namely an +escaping mechanism into other languages. It is true that the examples in the paper are essentially trivial; they are chosen for didactic reasons. The initial motivation for the development is a set of sTeX notes for a course of computation logic which cover parts of the LATIN logic atlas, and would profit -enormously from MMT inclusons. With the system, we can now undertake the case study, which +enormously from MMT inclusions. With the system, we can now undertake the case study, which is outside the scope of a systems paper. We will discuss this application in the paper. diff --git a/structural-extensions/rebuttal.txt b/structural-extensions/rebuttal.txt index 9bc4e41..659e8b1 100644 --- a/structural-extensions/rebuttal.txt +++ b/structural-extensions/rebuttal.txt @@ -10,49 +10,49 @@ not well motivated (OK) ---------------- Rebuttal ---------------- We thank the reviewers for their detailed and insightful reviews. -All reviewers had comments about poor readability due to the technical nature and of -lacking motivation/application. In particular: - -a. Reviewers 3/4/5 want to know about services/improvements to the ITP and MKM -communities. We believe it is desirable to build a framework in which all languages -(ITP/CAS/MKM) can be naturally represented. Our experience (especially in the OAF project, -where we import ITP libraries: Mizar, HOL Light, Coq, PVS, etc.) has shown that a mechanism -like the one proposed is indispensable to bring order into the zoo of language -features. This was clear to us, but must be clarified in the introduction. - -b. Reviewer 1 asks about the rationale behind the specific extensions and related work: Many -ITP/MKM systems have ad-hoc elaboration-based language features, that differ between -systems. Our contribution is a uniform mechanism that subsumes them and can serve for -systematic modelling of such features and as a basis for establishing interoperability -between ITP/MKM languages. - -We believe that we can remedy motivation and readability of the technical contribution by -improving the introduction (in terms of a) and b)), moving examples forward, and -systematically moving technical details to a separate section at the end so that the main -contribution of the paper becomes self-contained. This will also give us a chance for -further clarification of the syntax. - -Particulars: - -Reviewer 1 asks about completeness of the characterization: The proposed design and -features are evaluated with respect to the OAF examples. For these the design is adequate -and the main declaration-level language features are all covered. We acknowledge and will -discuss in the paper that there is a trade-off between completeness, modelling accuracy, -and tractability of the framework. +Motivation: -Reviewer 1 asks about "not every feature can be defined in all detail" this is caused by -the page limit, not the framework; we will clarify this in the paper. +One common issue was the insufficient discussion motivating our design choice and +its benefits for the community: Reviewer 1 asks about the rationale behind the +specific extensions and related work while Reviewers 3/4/5 inquire about +services/improvements to the ITP/MKM communities. -Reviewer 3: we will update the web page. +We believe it is desirable to build a framework in which all ITP/CAS/MKM languages +can be naturally and uniformly represented. Many ITP/MKM systems have various elaboration-based language features, but they are ad-hoc and differ between systems +Our experience (especially in the OAF project, where we import ITP libraries: Mizar, HOL Light, PVS, Coq, etc.) +has shown that a framework like we propose is indispensable to bring order into the zoo of language features. +The design and implementation of structural features as a mechanism for systematically modeling and studying such language features is motivated by this experience. +It also allows reusing our existing generic applications and services +(eg. IDE, search, change management, type checking). We will clarify this in the introduction. + +Readability: + +Another common issue was the readability and self-containedness of the paper. +Currently, we describe the intricacies of the formalism before giving sufficient motivation and concrete examples. + +We believe we can remedy this by improving the introduction and motivation along the lines described above, +moving the examples section forward, and systematically moving technical details (inference system) to a separate section at the end. +Therefore, the main contribution of the paper becomes self-contained. This will also let us further clarify the syntax. -Reviewer 5 mentions ambiguity between the "definition 1" in the example and the first -definition of the paper. Of course we will fix this. +Other Issues: -Reviewer 6 is concerned about locality and compositionally. +Reviewer 6 is concerned about locality and compositionality. Elaboration reduces the semantics of each structural feature to that of MMT. Thus, all categorical constructions of the category of MMT theories remain possible. However, it is desirable to have a notion of theory morphism that allows working with -structural features directly (i.e., without elaborating them). We wrote a section +structural features directly (without elaborating them). We wrote a section that provides sufficient conditions for that but removed it because it made the paper too -long and too technical. We will add a brief discussion of that in the final version. +long and too technical. We will add a brief discussion of that. + +Reviewer 1 asks about completeness of the characterization. +The proposed design and features are evaluated with respect to the OAF libraries: For these the design is adequate +and the main declaration-level language features are all covered. However, there is a trade-off between completeness, +modeling accuracy, and tractability of the framework. We will discuss this in the paper. + +Reviewer 1 asks about "not every feature can be defined in all detail" this is caused by +the page limit, not the framework; we will clarify this. + +Reviewer 3: we will update the web page. +Reviewer 5 mentions ambiguity between the definition numbering in the example and the paper. +We will fix this alongside all other minor comments the reviewers had. -- GitLab