The Coq mailing list

[Arnaud Spiwack <arnaud AT spiwack.net>]

(cc-ed on Coq-club in case someone interested would not read coqdev, however if you are not following Coq's developpement or at least aren't an active Ltac hacker, this mail probably won't interest you)


The branch new-tacticals (which was the main subject of the last "GT", see here: http://coq.inria.fr/cocorico/CoqDevelopment/CRGTCoq20120920 ) is now available publicly on github ( https://github.com/aspiwack/coq ). And I'm certainly accepting pull requests (it will be rebased 
frequently on the trunk from the official github coq mirror) as I've reached a point where my own perspective is not enough.

The branch brings to Ltac the potential of the new tactic type. Highlights are:

• A new refine tactic which doesn't use its own typechecking algorithm. It is, in particular, complete in the sense that all remaining evars are turned into goals (even if the evar appears in the type of another goal).
• Multiple-goal to multiple-goal tactics. It isn't really used yet, it could allow to write tactics that permutes the current goals, or a version of eauto which is aware that backtracking in some goal can help solve another one (this only works partially for the moment). An avatar of this feature, though, is that you can write "all:tac" to apply "tac" to all the focused subgoals (it can also be made the default).
  
• Backtracking: tactics can now be seen as succeeding multiple time (if a latter tactic fails, it can give it more success). It is useful to define tactics like "constructor": is constructor which can be applied is a success of the tactic. Not used yet (but it can readily be reused for typeclass eauto).
• At the Ocaml level: tactics can return a value, and are then sequence with a monadic sequencing operator.

Remarks:

• The new refine tactic reveals the internal of the pattern-matching compilation, which is often problematic, a cleaner version of the latter is in preparation so that refine works at least as well as the previous one.
• There are a few remaining bugs. If you find one, just send me an email.
• If you have an ocaml plugin, it almost certainly won't compile against this branch. I haven't written a porting tutorial yet, but if you are super-motivated, the relevant file is proofs/proofview.mli (you might also be interested in the submodules Tacmach.New and Tacticals.New).

Issue: performance-wise, the branch doesn't compare well to trunk. For now, I've observed a ~15% longer compiling time for the Coq archive. I
haven't checked on big contribs yet (it may or may not be ugly).

We did a bit of profiling last week with Pierre Letouzey, and we've isolated two tactics which are much slower (3 to 4 time so): tauto and
fourier, though we have only very small example, so the results might be skewed. We haven't found evidence, yet, that auto or rewrite have been slowed down significantly, but I still suspect them. Tauto and fourier are interesting though, because they are very different: tauto
is written essentially in Ltac and hence uses all the new tacticals, hence the new bureaucratie attached, whereas fourier is written entirely in ML, and has been little affected by the branch (all thetacticals it uses are old style, only at the "leaves" does it use
intro, or contradiction, or such which are cast to old style with Proofview.V82.of_tactic). So they might highlight different inefficiencies in the new implementation.

Overall, what we noticed, trying to be a bit finer is that there is no single point of slowdown, the extra time seems to be pretty diluted. One potential problem is the monadic style, which is good for the abstraction barrier, imposes writing a larger number of static closures which Ocaml is pretty bad at optimising. This issue was 
particularly obvious when I defined the underlying monad: it's a bit tricky to get all to work together, so I basically implemented it as a stack of monad transformers, but that makes a lot of intermediate closure that Ocaml doesn't know how to optimise away. As a result the
implementation was almost 10% slower than it currently is, I regained it by "manual inlining" (which I did by implementing the whole monad stack in Coq, and then applying Eval compute to each exported function).







A few potential issues I've noticed:

• The old ltac was pretty careful where to do "nf_evar" because it is costly, as a consequence, in the _expression_ t1;t2, the tactic "t2" couldn't see that t1 had instantiated evars. Doing nf_evar on goals doesn't really make sense in the new implementation, so when entering a tactic coded with the old type, my "emulator" starts by doing nf_evar, which may be costly. My guess is that we shouldn't do any more nf_evar automatically, instead tactic that need it can request it when needed. One way to achieve this would be to replace "constr" by some abstract "constr_in_evar_map" (equal to constr, but signaling that it may have defined evars) in the return type of tactic-building-things, and having a variant of "kind_of_term" for these which goes into the "evar_map" when some evar is exposed.
• The "split" primitive, due to technical reasons (it depends on Coq axioms which are realised at extraction as functions), is not very well inlined. It is the primitive used to implement "tclORELSE", so making it faster may help.
• Because of the possibility of dependent subgoals, every time a tactic is applied to a particular goal, it must first be checked whether the goal has already been solved. This process is significantly complicated by the semantics of clear. Indeed, when clearing an hypothesis (say "x") in a goal where there is an evar, the evar is modified as well, so that x is not present in its context either (otherwise, one could introduce a new variable "x" and use it to instantiate said evar, which is unsound). Another option is to fail if some evar depends on "x", but it's not very satisfactory either. Anyway, the issue here is that we're creating a new evar, but we don't want to create a new goal, so we basically have to tell the goal corresponding to the evar (if it exists) that it has been cleared so that it can know it correspond to a new evar. As it is done very often, it may also be better to find another semantics of clear which would avoid invading the execution of every tactic.

I could use help on:

• Any of the above.
• Ocaml 4 profiling: as Ocaml 4.0 has some modification over partial application, we may get different result when comparing the trunk to new-tacticals. Better, worse, or probably nothing. Yet it'd be nice to know.
• Large examples of tauto/fourier/auto/rewrite: so far, the examples we have used to measure slowdown run in well under a second. It would be useful to know what happen when we scale up to hard problems. So if you have such examples (preferably not requiring a plugin, so that they can be run without hacking), please contribute them.
• A better representation for evar_map: as queries into evar_map are becoming timewise significant, it might be a good idea to experiment with other datatypes (I'm thinking maybe splay trees could be nice as evar_map are typically very big, but we probably query only a few elements most of the time).
• Anything you feel like really.

Arnaud

--

'When I use a word,' Humpty Dumpty said in rather a scornful tone, 'it means just what I choose it to mean—neither more nor less.'

- Through the looking glass and what Alice found there, Lewis Caroll