The Coq mailing list

[Lasse Blaauwbroek <lasse AT blaauwbroek.eu>]

On 8/22/21 12:47 AM, Adam Chlipala wrote:
> On 8/21/21 4:20 PM, Lasse Blaauwbroek wrote:
> > (3) We actually face the opposite problem you face. While you are 
> > unable to find stable/usable systems to work with, we are (largely) 
> > unable to find end-users that are willing to give serious and 
> > recurring feedback on our systems while using it on complex 
> > developments. Part of the reason for this is the standard chicken/egg 
> > problem. Additionally, it seems that Coq users seem more unwilling to 
> > install/use plugins than users of other ITP's. For example, the 
> > Isabelle hammer is quite popular with it's users. One possible reason 
> > for this is that it is quite a barrier to install a plugin from Opam 
> > (especially when a user normally uses a version of Coq packaged by a 
> > unix distro or windows binary).
>
> An interesting point!  Let me just say that my collaborators and I are 
> very interested in trying out effective automation tools for Coq.  My 
> current bias is that it makes sense that SMT solvers would help, and 
> I'm unclear on the payoff from applying machine learning.  That is, 
> almost all of the subgoals that I can imagine being solvable by 
> mishmashing previously seen proofs (my crude model of what machine 
> learning would do) are also solvable by one or both of SMT solvers or 
> reasonable Ltac scripts.
You are right that custom Ltac scripts are probably hard to beat (at 
least for now). The more time one spends developing a suite of such 
tactics, the harder it will be to beat. With Tactician, we decided that 
if we cannot beat that, we should join it. Tactician will automatically 
learn to use your custom Ltac definitions in its proof search. That way, 
you can teach it your domain-specific knowledge. I would be extremely 
curious to know wether or not this actually works for you in practice. 
And if not, I'd like to know at what point it breaks down.