The Coq mailing list

[Théo Zimmermann <theo AT irif.fr>]

Doc of only: https://coq.inria.fr/refman/proof-engine/ltac.html#coq:tacn.only

Le lun. 7 déc. 2020 à 15:27, Lasse Blaauwbroek <lasse AT blaauwbroek.eu> a écrit 
:
>
> I assume that you are seeing 'only' as part of the 'search with cache' 
> tactic, and not as output of Suggest (if so that would be a bug).
>
> The 'only' tactical is not really part of the proof that is found, but some 
> glue to assemble the entire proof from the individual tactics. 'only n t' 
> runs t on the n-th goal. Currently, in Tactician n is always one, which 
> means that every tactic is always only run on the first goal. The reason it 
> is done like this is just a consequence of the internal search procedure of 
> Tactician. Also, 'only' is not special to Tactician, but can be used 
> everywhere.
>
> On 12/7/20 3:17 PM, Agnishom Chattopadhyay wrote:
>
> Thanks again, everyone. When I tried --unlock-base, it finally worked.
>
> By the way, what is the `only` tactical that Tactician seems to be 
> suggesting? Is this something that can be used without the presence of the 
> Tactician?
>
> On Sun, Dec 6, 2020 at 4:29 PM Laurent Thery <Laurent.Thery AT inria.fr> wrote:
>>
>>
>> Hi,
>>
>>
>> maybe you can save the state of the current switch on a file
>>
>> with
>>
>>  opam switch export state_file
>>
>> and then when you are in the new switch recreate the environment with :
>>
>>  opam switch import state_file
>>
>>
>> On 12/6/20 11:18 PM, Agnishom Chattopadhyay wrote:
>> > Thanks for your responses. I believe the problem here is that my OCaml
>> > compiler is 4.07.
>> >
>> > I suppose I could create a new opam switch but I already have
>> > coq-platform installed on this switch, and everything works. Is it not
>> > possible to upgrade my ocamlc to 4.08 in the existing switch?
>> >
>> > On Sun, Dec 6, 2020 at 3:47 PM Lasse Blaauwbroek <lasse AT blaauwbroek.eu
>> > <mailto:lasse AT blaauwbroek.eu>> wrote:
>> >
>> >     The most likely culprits are (1) Your opam version is 1.x, in which
>> >     case you should upgrade to 2.x (2) Your OCaml compiler is too old
>> >     (you need at least 4.08). In this case, you can try to install
>> >     Tactician in a new switch (which will create a new stack of OCaml
>> >     software, orthogonal to anything you might have already installed):
>> >
>> >     opam switch create coq-tactician-switch --empty
>> >     eval $(opam env)
>> >     opam repo add coq-released https://coq.inria.fr/opam/released
>> >     <https://coq.inria.fr/opam/released>
>> >     opam install coq-tactician
>> >
>> >     If that does not work either, please post the output of 'opam config
>> >     report' and 'opam install coq-tactician --debug'.
>> >
>> >     Regards,
>> >     Lasse
>> >
>> >     On 12/6/20 10:27 PM, Agnishom Chattopadhyay wrote:
>> >>     Thanks for the announcement. This seems like a very useful tool.
>> >>
>> >>     When I try to install, I get a very non-descript error message.
>> >>
>> >>     agnishom@agnishomDuncan:~$ opam install coq-tactician
>> >>     Sorry, no solution found: there seems to be a problem with your
>> >>     request.
>> >>
>> >>     No solution found, exiting
>> >>
>> >>     I tried this after doing opam update and opam upgrade, but that
>> >>     didn't help.
>> >>
>> >>     On Sun, Dec 6, 2020 at 2:14 PM Lasse Blaauwbroek
>> >>     <lasse AT blaauwbroek.eu <mailto:lasse AT blaauwbroek.eu>> wrote:
>> >>
>> >>         We would like to announce Tactician 1.0 beta1, the first 
>> >> official
>> >>         release of Tactician. See the website here
>> >>         https://coq-tactician.github.io
>> >>         <https://coq-tactician.github.io> and an online demo here
>> >>         https://coq-tactician.github.io/demo.html
>> >>         <https://coq-tactician.github.io/demo.html>
>> >>
>> >>         Tactician is a tactic learner and prover for the Coq Proof
>> >>         Assistant.
>> >>         The system will help users make tactical proof decisions while
>> >>         they
>> >>         retain control over the general proof strategy. To this end,
>> >>         Tactician
>> >>         will learn from previously written tactic scripts, and either
>> >>         gives the
>> >>         user suggestions about the next tactic to be executed or
>> >>         altogether
>> >>         takes over the burden of proof synthesis. Tactician’s goal is
>> >>         to provide
>> >>         the user with a seamless, interactive, and intuitive
>> >>         experience together
>> >>         with strong, adaptive proof automation.
>> >>
>> >>         Even though a lot still remains to be done, with this version
>> >>         we believe
>> >>         that the system is mature enough to be used in real
>> >>         developments. We
>> >>         would like to solicit any feedback on the system you might have.
>> >>
>> >>         Tactician is available for Coq v8.11, v8.12, v8.13 and master
>> >>         and on
>> >>         Linux, macOS and Windows. Installation instructions can be
>> >>         found in the
>> >>         manual (https://coq-tactician.github.io/manual
>> >>         <https://coq-tactician.github.io/manual>). Tactician has
>> >>         first-class support for Opam (Coq's package manager), and can
>> >>         automatically learn from almost any Coq package. For the
>> >>         exceptions,
>> >>         special support can be added. Currently, special support
>> >>         exists for the
>> >>         HoTT homotopy type theory library. If tactician cannot
>> >>         instrument your
>> >>         favorite package and you would like to see support, please
>> >>         open an issue.
>> >>
>> >>         -- Future direction --
>> >>
>> >>         This release of Tactician is aimed at providing Coq users with
>> >>         an easy
>> >>         to use system that can be used in real Coq developments. The
>> >>         next step
>> >>         in our grand plan is to transform Tactician into a machine
>> >>         learning
>> >>         platform, where AI-researchers can add agents to Tactician (a
>> >>         plugin for
>> >>         a plugin) using an easy-to-use API. The goal of this API is to
>> >>         take away
>> >>         the hard Coq engineering problems and only leave the hard 
>> >> machine
>> >>         learning problems.
>> >>
>> >>         This API is still under heavy development. We are therefore
>> >>         not yet
>> >>         inviting the wider AI-community to work with Tactician.
>> >>         However, we are
>> >>         looking for collaborators/beta-testers. So if you have a good
>> >>         machine
>> >>         learning idea that you would like to implement on top of
>> >>         Tactician,
>> >>         please get in touch.
>> >>
>> >>         Lasse Blaauwbroek
>> >>