The Coq mailing list

[Lasse Blaauwbroek <lasse AT blaauwbroek.eu>]

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
>>