Installation issues -- No package named coq-hammer-tactics found

[brando90]

I was following the video tutorial but got this issue:

→  hammer_switch                          ocaml-base-compiler.4.12.0  hammer_switch
(meta_learning) brandomiranda~/sketching-learning-coq ❯ opam install coq-hammer-tactics 
[ERROR] No package named coq-hammer-tactics found.

How do I install CoqHammer?

[brando90]

I get it's there but can't load it on my vscode coq (since coqide can't be installed in the mac m1 chip macbook):

(meta_learning) brandomiranda~/Downloads/platform-2022.01.0 ❯ opam install coq-hammer-tactics
[WARNING] Opam package conf-python-3.9.0.0 depends on the following system package that can no longer be found: python@3
[NOTE] Package coq-hammer-tactics is already installed (current version is 1.3.2+8.15).

I see

Cannot find a physical path bound to logical path matching suffix
<> and prefix Hammer.
Not in proof mode.

[brando90]

I do see coqhammer in my opam list

(meta_learning) brandomiranda~/coq4brando ❯ opam list
# Packages matching: installed
# Name                    # Installed     # Synopsis
base-bigarray             base
base-threads              base
base-unix                 base
camlp5                    7.14            Preprocessor-pretty-printer of OCaml
conf-adwaita-icon-theme   2               Virtual package relying on adwaita-icon-theme
conf-autoconf             0.1             Virtual package relying on autoconf installation
conf-automake             1               Virtual package relying on GNU automake
conf-bison                2               Virtual package relying on GNU bison
conf-boost                1               Virtual package relying on boost
conf-cairo                1               Virtual package relying on a Cairo system installation
conf-findutils            1               Virtual package relying on findutils
conf-flex                 2               Virtual package relying on GNU flex
conf-g++                  1.0             Virtual package relying on the g++ compiler (for C++)
conf-gcc                  1.0             Virtual package relying on the gcc compiler (for C)
conf-gmp                  4               Virtual package relying on a GMP lib system installation
conf-gtk3                 18              Virtual package relying on GTK+ 3
conf-gtksourceview3       0+2             Virtual package relying on a GtkSourceView-3 system installation
conf-libtool              1               Virtual package relying on libtool installation
conf-mpfr                 3               Virtual package relying on library MPFR installation
conf-perl                 2               Virtual package relying on perl
conf-pkg-config           2               Check if pkg-config is installed and create an opam switch local pkgconfig folder
conf-python-3             9.0.0           Virtual package relying on Python-3 installation
conf-which                1               Virtual package relying on which
coq                       8.15.0          Formal proof management system
coq-aac-tactics           8.15.0          Coq tactics for rewriting universally quantified equations, modulo associative (and possibly commutative and idempotent) operators
coq-bignums               8.15.0          Bignums, the Coq library of arbitrary large numbers
coq-compcert              3.10            The CompCert C compiler (64 bit)
coq-coqeal                1.1.0           CoqEAL - The Coq Effective Algebra Library
coq-coqprime              1.1.1           Certifying prime numbers in Coq
coq-coqprime-generator    1.1.1           Certificate generator for prime numbers in Coq
coq-coquelicot            3.2.0           A Coq formalization of real analysis compatible with the standard library
coq-corn                  8.13.0          The Coq Constructive Repository at Nijmegen
coq-dpdgraph              1.0+8.15        Compute dependencies between Coq objects (definitions, theorems) and produce graphs
coq-elpi                  1.12.1          Elpi extension language for Coq
coq-equations             1.3+8.15        A function definition package for Coq
coq-ext-lib               0.11.6          A library of Coq definitions, theorems, and tactics
coq-flocq                 3.4.3           A formalization of floating-point arithmetic for the Coq system
coq-gappa                 1.5.1           A Coq tactic for discharging goals about floating-point arithmetic and round-off errors using the Gappa prover
coq-hammer                1.3.2+8.15      General-purpose automated reasoning hammer tool for Coq
coq-hammer-tactics        1.3.2+8.15      Reconstruction tactics for the hammer for Coq
coq-hierarchy-builder     1.2.1           High level commands to declare and evolve a hierarchy based on packed classes
coq-hott                  8.15            The Homotopy Type Theory library
coq-interval              4.4.0           A Coq tactic for proving bounds on real-valued expressions automatically
coq-iris                  3.6.0           A Higher-Order Concurrent Separation Logic Framework with support for interactive proofs
coq-iris-heap-lang        3.6.0           The canonical example language for Iris
coq-libhyps               2.0.4           Hypotheses manipulation library
coq-math-classes          8.15.0          A library of abstract interfaces for mathematical structures in Coq
coq-mathcomp-algebra      1.14.0          Mathematical Components Library on Algebra
coq-mathcomp-analysis     0.3.13          An analysis library for mathematical components
coq-mathcomp-bigenough    1.0.1           A small library to do epsilon - N reasoning
coq-mathcomp-character    1.14.0          Mathematical Components Library on character theory
coq-mathcomp-field        1.14.0          Mathematical Components Library on Fields
coq-mathcomp-fingroup     1.14.0          Mathematical Components Library on finite groups
coq-mathcomp-finmap       1.5.1           Finite sets, finite maps, finitely supported functions
coq-mathcomp-multinomials 1.5.5           A Multivariate polynomial Library for the Mathematical Components Library
coq-mathcomp-real-closed  1.1.2           Mathematical Components Library on real closed fields
coq-mathcomp-solvable     1.14.0          Mathematical Components Library on finite groups (II)
coq-mathcomp-ssreflect    1.14.0          Small Scale Reflection
coq-mathcomp-zify         1.2.0+1.12+8.13 Micromega tactics for Mathematical Components
coq-menhirlib             20211230        A support library for verified Coq parsers produced by Menhir
coq-mtac2                 1.4+8.15        Mtac2: Typed Tactics for Coq
coq-paramcoq              1.1.3+coq8.15   Plugin for generating parametricity statements to perform refinement proofs
coq-quickchick            1.6.0           Randomized Property-Based Testing Plugin for Coq
coq-reglang               1.1.3           Representations of regular languages (i.e., regexps, various types of automata, and WS1S) with equivalence proofs, in Coq and MathComp
coq-simple-io             1.6.0           IO monad for Coq
coq-stdpp                 1.7.0           An extended "Standard Library" for Coq
coq-unicoq                1.6+8.15        An enhanced unification algorithm for Coq
coq-unimath               20210807        Library of Univalent Mathematics
coq-vst                   2.9             Verified Software Toolchain
cppo                      1.6.8           Code preprocessor like cpp for OCaml
csexp                     1.5.1           Parsing and printing of S-expressions in Canonical form
dune                      3.0.3           Fast, portable, and opinionated build system
dune-configurator         3.0.3           Helper library for gathering system configuration
elpi                      1.13.8          ELPI - Embeddable λProlog Interpreter
eprover                   2.6             E Theorem Prover
gappa                     1.4.0           Tool intended for formally proving properties on numerical programs dealing with floating-point or fixed-point arithmetic
gmp-ecm                   7.0.3           GMP-ECM library for the Elliptic Curve Method (ECM) for integer factorization
menhir                    20211230        An LR(1) parser generator
menhirLib                 20211230        Runtime support library for parsers generated by Menhir
menhirSdk                 20211230        Compile-time library for auxiliary tools related to Menhir
num                       1.4             The legacy Num library for arbitrary-precision integer and rational arithmetic
ocaml                     4.10.2          The OCaml compiler (virtual package)
ocaml-base-compiler       4.10.2          Official release 4.10.2
ocaml-compiler-libs       v0.12.4         OCaml compiler libraries repackaged
ocaml-config              1               OCaml Switch Configuration
ocaml-migrate-parsetree   1.8.0           Convert OCaml parsetrees between different versions
ocamlbuild                0.14.1          OCamlbuild is a build system with builtin rules to easily build most OCaml projects
ocamlfind                 1.9.3           A library manager for OCaml
ocamlgraph                2.0.0           A generic graph library for OCaml
ppx_derivers              1.2.1           Shared [@@deriving] plugin registry
ppx_deriving              5.1             Type-driven code generation for OCaml
ppxlib                    0.15.0          Standard library for ppx rewriters
re                        1.10.3          RE is a regular expression library for OCaml
result                    1.5             Compatibility Result module
seq                       base            Compatibility package for OCaml's standard iterator type starting from 4.07.
sexplib0                  v0.14.0         Library containing the definition of S-expressions and some base converters
stdlib-shims              0.3.0           Backport some of the new stdlib features to older compiler
zarith                    1.12            Implements arithmetic and logical operations over arbitrary-precision integers

but vscode is not able to find it...wonder what coq version vscode is pointing to?

[brando90]

coq top path is

/Users/brandomiranda/.opam/__coq-platform.2022.01.0~8.14~2022.01/bin

and path is

(meta_learning) brandomiranda~/coq4brando ❯ echo $PATH
/Users/brandomiranda/.opam/__coq-platform.2022.01.0~8.15~beta1/bin:/Users/brandomiranda/opt/anaconda3/envs/meta_learning/bin:/opt/homebrew/bin:/usr/bin:/bin:/usr/sbin:/sbin

[brando90]

I changed it to the one matching the path but it still does not work...

Cannot find a physical path bound to logical path matching suffix
<> and prefix Hammer.
Not in proof mode.

[brando90]

ok I tried it in coqtop and it seemed to work:

(meta_learning) brandomiranda~/coq4brando ❯ coqtop
Welcome to Coq 8.15.0

Coq < From Hammer Require Import Tactics.
[Loading ML file ring_plugin.cmxs ... done]
[Loading ML file zify_plugin.cmxs ... done]
[Loading ML file micromega_plugin.cmxs ... done]
[Loading ML file ssrmatching_plugin.cmxs ... done]
[Loading ML file ssreflect_plugin.cmxs ... done]
[Loading ML file hammer_lib.cmxs ... done]
[Loading ML file hammer_tactics.cmxs ... done]

Coq < Print sauto.
Ltac sauto := <hammer_tactics::Hammer_sauto@0> missing printer

so perhaps it's just vscode? which is weird cuz it's pointing to the right coqtop afaik...

[brando90]

Ok I fixed it I think. This is what I did:

1. create a new switch opam switch create hammer_switch ocaml-base-compiler.4.12.0 and made sure I had xcode & hombrew/brew.
2. I installed the coq plataform using their binaries https://github.com/coq/platform/blob/main/doc/README_macOS.md and ran bash coq_platform_make.sh
3. updated my path with $(opam env)
4. then installed coqhammer opam install coq-hammer-tactics
5. then made sure the coqtop path in the vscode settings had the path from my PATH e.g. /Users/brandomiranda/.opam/__coq-platform.2022.01.0~8.15~beta1/bin
6. restarted vscode several times to make sure it was running the above path.
7. ran From Hammer Require Import Tactics. then coq ran no error.

[brando90]

trying to unify to SO as an answer: https://stackoverflow.com/questions/71343424/how-to-tell-vscode-where-coq-is-fixing-could-not-start-coqtop-coqtop