Quick mode?

[gmalecha]

Would it be possible to implement a "quick mode" which would not have any movies but not require building the entire file? E.g. if I've already built my development with coqc, then it would be nice to be able to get non-movie versions generated very quickly.

[cpitclaudel]

Sure, in fact we almost already have this with minimal.py. Which frontend do you use? The command line, sphinx, pelican, or something else?

[gmalecha]

I just started using the command line. ./alectryon.py tmp.v

[cpitclaudel]

Ah, neat, got it. Yes, I can add a flag to skip processing of inputs and outputs. Is this for proofs that change a lot? 'cause otherwise --cache-directory=. is usually enough for me.

[gmalecha]

They don't change really frequently, but its often the case that we are switching branches to look at something and some things might be stale.

I have a very tiny patch that disables them, but I couldn't find a nice way to get the configuration from the command line.

I know I shouldn't do this, but this was my (incredibly hacky) patch.

diff --git a/alectryon/cli.py b/alectryon/cli.py
index 3ce5d3e..037c001 100755
--- a/alectryon/cli.py
+++ b/alectryon/cli.py
@@ -580,6 +580,11 @@ and produce reStructuredText, HTML, or JSON output.""")
     parser.add_argument("--cache-directory", default=None, metavar="DIRECTORY",
                         help=CACHE_DIRECTORY_HELP)
 
+    MOVIES_HELP = ("Produce proof movies.")
+    parser.add_argument("--movies", default=True, metavar="MOVIES",
+                        help=MOVIES_HELP)
+
+
     NO_HEADER_HELP = "Do not insert a header with usage instructions in webpages."
     parser.add_argument("--no-header", action='store_false',
                         dest="include_banner", default="True",
diff --git a/alectryon/core.py b/alectryon/core.py
index 37dd343..0e5fd8a 100755
--- a/alectryon/core.py
+++ b/alectryon/core.py
@@ -88,13 +88,15 @@ class SerAPI():
 
     def __init__(self, args=(), # pylint: disable=dangerous-default-value
                  sertop_bin=SERTOP_BIN,
-                 pp_args=DEFAULT_PP_ARGS):
+                 pp_args=DEFAULT_PP_ARGS,
+                 produce_movie=True):
         """Configure and start a ``sertop`` instance."""
         self.args, self.sertop_bin = [*args, *SerAPI.DEFAULT_ARGS], sertop_bin
         self.sertop = None
         self.next_qid = 0
         self.pp_args = {**SerAPI.DEFAULT_PP_ARGS, **pp_args}
         self.last_response = None
+        self.produce_movie = produce_movie
 
     def __enter__(self):
         self.reset()
@@ -327,8 +329,11 @@ class SerAPI():
             if span_id is None:
                 fragments.append(Text(contents, loc=loc))
             else:
-                messages.extend(self._exec(span_id, chunk))
-                goals = list(self._goals(span_id, chunk))
+                if self.produce_movie:
+                    messages.extend(self._exec(span_id, chunk))
+                    goals = list(self._goals(span_id, chunk))
+                else:
+                    goals = None
                 fragment = Sentence(contents, loc=loc, messages=[], goals=goals)
                 fragments.append(fragment)
                 fragments_by_id[span_id] = fragment
diff --git a/alectryon/transforms.py b/alectryon/transforms.py
index 3a5a5ab..274ea52 100755
--- a/alectryon/transforms.py
+++ b/alectryon/transforms.py
@@ -243,9 +243,12 @@ def attach_comments_to_code(fragments, predicate=lambda _: True):
 
 def fragment_goal_sets(fr):
     if isinstance(fr, RichSentence):
-        yield from (gs.goals for gs in fr.outputs if isinstance(gs, Goals))
+        yield from (gs.goals for gs in fr.outputs if isinstance(gs, Goals) and not (gs.goals is None))
     if isinstance(fr, Sentence):
-        yield fr.goals
+        if fr.goals is None:
+            yield []
+        else:
+            yield fr.goals
 
 def fragment_message_sets(fr):
     if isinstance(fr, RichSentence):

[cpitclaudel]

That a reasonable patch, though I think it might be even better to bypass SerAPI completely if we don't need it. I had some code on a Lean branch to be more agnostic wrt the prover that we're using to execute sentences; the best might be to merge that in and make a null prover. Let me look into it.

[gmalecha]

I think you still need SerAPI to do the lexing, at least for what I'm using it for.

[cpitclaudel]

Can you explain? What advantage to you get from properly segmenting sentences if you then just display them?

[gmalecha]

I have another patch that adds location information to the output, e.g. <span class="alectryon-sentence" location="23_35">...</span> and I reference this information to overlay performance data output by Coq's timing. Having a way to identify sentences seems like it could be very nice way to integrate custom data sources. If you're interested, I should be able to submit a PR.

[cpitclaudel]

Oh, cool stuff! So, let's see. I think your patch is pretty good. To pass the data from th command line you have two options: the easy way is just make that a class-level constant of SerAPI and set it just like SerAPI.EXPECT_UNEXPECTED. The cleaner version is to generalize annotate(), which I've done in the lean3 branch. Beyond that you can simplify the patch a bit by defaulting to [] instead of None for the goals I think.

[gmalecha]

Can I build an MR off of that branch? I don't see it on master.

[cpitclaudel]

The lean3 branch isn't ready for merging, no (we have a student working on it this summer). I think we can go with the first option and then clean things up once we have the lean branch ready in a few months.

[cpitclaudel]

I think this should be trivial to do by piggy-backing off of the work for I did #60 (which lets you pick a driver). You would add a driver inheriting from SerAPI that doesn't process messages. You'd need to:

1. Add a subclass of SerAPI in serapi.py
2. Override the _exec and _goals methods to return empty lists.
3. Add this new driver to DRIVERS_BY_LANGUAGE in core.py

But now that I write this I realize it's really just 5 lines, so I pushed the patch to https://github.com/cpitclaudel/alectryon/tree/gh-60-coqc : c5431ab#diff-9f4631f8b9aee89150ee816a0a5bf0a3a10b5e6d971bf27802f2715cdfd15311R327-R338

Can you give it a try?

[cpitclaudel]

Pushed to master with attribution under the option --coq-driver sertop_noexec. Thanks for the nice idea!