The Coq mailing list

[Valentin Robert <valentin.robert.42 AT gmail.com>]

It is described in this paragraph:

http://coq.inria.fr/refman/Reference-Manual011.html#hevea_command244

- Valentin

On Tue, Aug 20, 2013 at 6:49 PM, Jason Gross 
<jasongross9 AT gmail.com>
 wrote:
> I'm glad it works.  Is the meaning of ::= documented somewhere in the
> reference manual?  What does it do?
>
> -Jason
>
> On Aug 20, 2013 2:38 AM, "t x" 
> <txrev319 AT gmail.com>
>  wrote:
>>
>> Jason: your idea worked.
>>
>>   Using the following, I can fake a "add only tactic database"
>>
>> ==== nuke.v
>>
>> Tactic Notation "nuke_tacs" := initial_set_of_tacs.
>>
>> Ltac nuke_update := nuke_tacs.
>>
>> Ltac nuke :=
>>   .... do some stuff ...;
>>   repeat (nuke_update || ... tacs ...);
>>   .... do some more stuff ... .
>>
>>
>> ==== to register a new tac
>>
>> Tactic Notation "nuke_tacs" := new_tac || nuke_tacs.
>>
>> (* Tactic Notation does not support recursion.
>>    Thus, the second nuke_tacs gets the old value. *)
>>
>> (* Now, we need to force the "nuke" tactic
>>    to use the latest nuke_tacs *)
>>
>> Ltac nuke_update ::= nuke_tacs.
>>
>> (* the ::= ensure taht nuke_update has the latest nuke_tacs; and forces
>>    nuke to use the latest nuke_update *).
>>
>>
>>
>>
>>
>> On Tue, Aug 20, 2013 at 6:29 AM, t x 
>> <txrev319 AT gmail.com>
>>  wrote:
>>>
>>> re re-binding:
>>>
>>>   I was
>>>
>>>   * playing with "Ltac ... ::=" (note the double ::), for examp;e
>>>
>>> Ltac nuke_split := new_tac || nuke_split
>>>
>>>   * getting stack overflows
>>>
>>>   * attributing said stack overflows to the 2nd nuke_split referring to
>>> the new rather than the old value (since Ltacs can recursively call 
>>> itself)
>>>
>>>   * however, perhaps Tactic Notation's inability to recurse might be
>>> useful in this case.
>>>
>>>   * I will re-investigate on this and report back.
>>>
>>> re plugins:
>>>
>>>   I'm going the OCaml route. If anyone knows of any tutorial besides
>>> http://gallium.inria.fr/blog/your-first-coq-plugin/ I would appreciate it.
>>> (It seems like the main difficulties is just understanding boiler plate.)
>>>
>>>
>>>
>>>
>>> On Tue, Aug 20, 2013 at 4:16 AM, Jason Gross 
>>> <jasongross9 AT gmail.com>
>>> wrote:
>>>>
>>>> Tactic notations can be rebound while making use of the old value.  For
>>>> example,
>>>> Ltac a := pose 1 as a.
>>>> Tactic Notation "nuke" := a.
>>>> Ltac b := pose 2 as b.
>>>> Tactic Notation "nuke" := (nuke; b).
>>>>
>>>> (As an aside, I have not figured out how to print the script of a tactic
>>>> notation.  Can someone tell me how to do this?)
>>>>
>>>> There is not currently a notion of a database of tactics, other than
>>>> those of auto or rewrite, so you'd have to write an OCaml plugin if you
>>>> wanted to use that path.  However, I vaguely recall this being mentioned 
>>>> on
>>>> coq-club in the past, and that there might be such custom databases in
>>>> future versions of Coq.  Someone more knowledgeable than I (or willing 
>>>> to do
>>>> more archive-digging) might be able to say more.
>>>>
>>>> -JAson
>>>>
>>>>
>>>> On Monday, August 19, 2013, t x wrote:
>>>>>
>>>>> Hi,
>>>>>
>>>>>   I have an tactic that looks something like:
>>>>>
>>>>> ===== nuke.v
>>>>> Ltac nuke = repeat ( tac1 || tac2 || tac3 || tac4 ).
>>>>>
>>>>>
>>>>>
>>>>> ===== foo.v
>>>>> Require Import nuke.
>>>>>
>>>>> Some definitions.
>>>>> Ltac foo_solver = ...
>>>>>
>>>>> I would now like to rebind:
>>>>>
>>>>> Ltac nuke = repeat (tac1 || tac2 || tac3 || tac4 || foo_solver).
>>>>>
>>>>>
>>>>> ===== bar.v
>>>>> Require Import nuke foo.
>>>>>
>>>>> Some definitions related to bar.
>>>>> Ltac bar_solver = ...
>>>>>
>>>>>
>>>>> I would now like to rebind:
>>>>>
>>>>> Ltac nuke = repeat (tac1 || tac2 || tac3 || tac4 || foo_solver ||
>>>>> bar_solver).
>>>>>
>>>>>
>>>>> #### What I've tried so far:
>>>>>
>>>>> Hint Extern <-- this does not appear to work because "auto" wants
>>>>> tactics that solves the subgoals. Whereas in my case, the job of each 
>>>>> tacX
>>>>> is to simplify/split the goal into simpler subgoals.
>>>>>
>>>>> #### What I'd like:
>>>>>
>>>>> I would like something similar to a Hint Rewrite Database.
>>>>>
>>>>> Something like:
>>>>>
>>>>> ===== nuke.v ...
>>>>> Hint Use tac1 : nukedb
>>>>> Hint Use tac2 : nukedb
>>>>>
>>>>> Ltac nuke = repeat with nukedb.
>>>>>
>>>>> ===== foo.v
>>>>>
>>>>> Hint Use foo_solver : nukedb.
>>>>>
>>>>> (at this point, "nuke" tactic also uses foo_solver
>>>>>
>>>>>
>>>>> ===== bar.b
>>>>>
>>>>> Hint Use bar_solver :nukedb.
>>>>>
>>>>> (at this point, "nuke" tactic also uses bar_solver)
>>>>>
>>>>>
>>>>> Is there a way to setup this up in Ltac, or does this go into the
>>>>> realms of Ocaml plugins?
>>>>>
>>>>> Thanks!
>>>
>>>
>>
>