lukaszcz/coqhammer issues and pull requests

#188 - Please pick the version you prefer for Coq 8.20 in Coq Platform 2025.01

Issue - State: closed - Opened by MSoegtropIMC 2 months ago

#187 - Please pick the version you prefer for Coq 8.20 in Coq Platform 2025.01

Issue - State: closed - Opened by MSoegtropIMC 2 months ago

#186 - Weird Github tar ball issues

Issue - State: closed - Opened by MSoegtropIMC 3 months ago - 11 comments

#185 - Adapt to https://github.com/coq/coq/pull/19530

Pull Request - State: open - Opened by proux01 5 months ago

#184 - Publish a release compatible with Coq 8.20

Issue - State: closed - Opened by SnarkBoojum 5 months ago - 1 comment

#183 - qauto breaks goal into multiple subgoals instead of solving or failing.

Issue - State: open - Opened by sakekasi 7 months ago - 1 comment
Labels: bug

#100 - Dependency prediction failed

Issue - State: closed - Opened by KevOrr almost 4 years ago - 7 comments

#100 - Dependency prediction failed

Issue - State: closed - Opened by KevOrr almost 4 years ago - 7 comments

#99 - Travis CI fails

Issue - State: closed - Opened by lukaszcz about 4 years ago
Labels: help wanted

#99 - Travis CI fails

Issue - State: closed - Opened by lukaszcz about 4 years ago
Labels: help wanted

#98 - 'use' option accepts lemmas with implicit arguments.

Pull Request - State: closed - Opened by ccyip about 4 years ago - 4 comments

#98 - 'use' option accepts lemmas with implicit arguments.

Pull Request - State: closed - Opened by ccyip about 4 years ago - 4 comments

#97 - Allow "use: ..." option to accept lemmas with implicit arguments?

Issue - State: closed - Opened by ccyip about 4 years ago - 4 comments

#97 - Allow "use: ..." option to accept lemmas with implicit arguments?

Issue - State: closed - Opened by ccyip about 4 years ago - 4 comments

#96 - Adapt w.r.t. coq/coq#13563.

Pull Request - State: closed - Opened by ppedrot about 4 years ago - 2 comments

#96 - Adapt w.r.t. coq/coq#13563.

Pull Request - State: closed - Opened by ppedrot about 4 years ago - 2 comments

#95 - Overlay for coq/coq#13377. Fixes Coq's timeout facilities

Pull Request - State: closed - Opened by LasseBlaauwbroek over 4 years ago - 1 comment

#95 - Overlay for coq/coq#13377. Fixes Coq's timeout facilities

Pull Request - State: closed - Opened by LasseBlaauwbroek over 4 years ago - 1 comment

#94 - remove vos, vok, and cache files in tests directories on clean

Pull Request - State: closed - Opened by palmskog over 4 years ago

#94 - remove vos, vok, and cache files in tests directories on clean

Pull Request - State: closed - Opened by palmskog over 4 years ago

#93 - Dune tests error: permission denied

Issue - State: closed - Opened by lukaszcz over 4 years ago - 1 comment

#93 - Dune tests error: permission denied

Issue - State: closed - Opened by lukaszcz over 4 years ago - 1 comment

#92 - Dune build error

Issue - State: open - Opened by lukaszcz over 4 years ago - 2 comments

#92 - Dune build error

Issue - State: open - Opened by lukaszcz over 4 years ago - 2 comments

#91 - switch from .mllib to .mlpack and remove Dune wrapping in 8.12

Pull Request - State: closed - Opened by palmskog over 4 years ago

#91 - switch from .mllib to .mlpack and remove Dune wrapping in 8.12

Pull Request - State: closed - Opened by palmskog over 4 years ago

#90 - Dune builds and tests for master

Pull Request - State: closed - Opened by palmskog over 4 years ago - 1 comment

#90 - Dune builds and tests for master

Pull Request - State: closed - Opened by palmskog over 4 years ago - 1 comment

#89 - OCaml module name clash between CoqHammer and Coq master (partac)

Issue - State: closed - Opened by palmskog over 4 years ago - 9 comments

#89 - OCaml module name clash between CoqHammer and Coq master (partac)

Issue - State: closed - Opened by palmskog over 4 years ago - 9 comments

#88 - Partition tests directory into plugin and tactics

Pull Request - State: closed - Opened by palmskog over 4 years ago - 1 comment

#88 - Partition tests directory into plugin and tactics

Pull Request - State: closed - Opened by palmskog over 4 years ago - 1 comment

#87 - Adjust Dune build flags and add tests via Dune for 8.12

Pull Request - State: closed - Opened by palmskog over 4 years ago - 1 comment

#87 - Adjust Dune build flags and add tests via Dune for 8.12

Pull Request - State: closed - Opened by palmskog over 4 years ago - 1 comment

#86 - Bug in the "hammer" tactic with parallel proof processing in CoqIDE (minor)

Issue - State: open - Opened by richardDap over 4 years ago - 1 comment
Labels: bug

#86 - Bug in the "hammer" tactic with parallel proof processing in CoqIDE (minor)

Issue - State: open - Opened by richardDap over 4 years ago - 1 comment
Labels: bug

#85 - opam installation failure: bad checksum

Issue - State: closed - Opened by lukaszcz over 4 years ago - 3 comments
Labels: bug, help wanted

#85 - opam installation failure: bad checksum

Issue - State: closed - Opened by lukaszcz over 4 years ago - 3 comments
Labels: bug, help wanted

#84 - Adapt w.r.t. coq/coq#12565.

Pull Request - State: closed - Opened by ppedrot over 4 years ago - 1 comment

#84 - Adapt w.r.t. coq/coq#12565.

Pull Request - State: closed - Opened by ppedrot over 4 years ago - 1 comment

#83 - standard Dune tactics build should not include Mathcomp.v

Pull Request - State: closed - Opened by palmskog over 4 years ago

#83 - standard Dune tactics build should not include Mathcomp.v

Pull Request - State: closed - Opened by palmskog over 4 years ago

#82 - Enable optional building of hammer and tactics using Dune for 8.12

Pull Request - State: closed - Opened by palmskog over 4 years ago

#82 - Enable optional building of hammer and tactics using Dune for 8.12

Pull Request - State: closed - Opened by palmskog over 4 years ago

#81 - update Travis CI configuration and opam packages for 8.10

Pull Request - State: closed - Opened by palmskog over 4 years ago

#81 - update Travis CI configuration and opam packages for 8.10

Pull Request - State: closed - Opened by palmskog over 4 years ago

#80 - update Travis CI configuration and opam packages for master

Pull Request - State: closed - Opened by palmskog over 4 years ago - 1 comment

#80 - update Travis CI configuration and opam packages for master

Pull Request - State: closed - Opened by palmskog over 4 years ago - 1 comment

#79 - update Travis CI configuration and opam packages for 8.11

Pull Request - State: closed - Opened by palmskog over 4 years ago

#79 - update Travis CI configuration and opam packages for 8.11

Pull Request - State: closed - Opened by palmskog over 4 years ago

#78 - update Travis CI configuration and opam packages for 8.12

Pull Request - State: closed - Opened by palmskog over 4 years ago

#78 - update Travis CI configuration and opam packages for 8.12

Pull Request - State: closed - Opened by palmskog over 4 years ago

#77 - sauto times out on reasonably small example

Issue - State: open - Opened by samuelgruetter over 4 years ago - 7 comments
Labels: enhancement

#77 - sauto times out on reasonably small example

Issue - State: open - Opened by samuelgruetter over 4 years ago - 7 comments
Labels: enhancement

#76 - Adapt w.r.t. coq/coq#12720.

Pull Request - State: closed - Opened by ppedrot over 4 years ago - 1 comment

#76 - Adapt w.r.t. coq/coq#12720.

Pull Request - State: closed - Opened by ppedrot over 4 years ago - 1 comment

#75 - Adapt w.r.t. coq/coq#12709.

Pull Request - State: closed - Opened by ppedrot over 4 years ago - 1 comment

#75 - Adapt w.r.t. coq/coq#12709.

Pull Request - State: closed - Opened by ppedrot over 4 years ago - 1 comment

#74 - Adapt to https://github.com/coq/coq/pull/11604

Pull Request - State: closed - Opened by maximedenes over 4 years ago - 1 comment

#74 - Adapt to https://github.com/coq/coq/pull/11604

Pull Request - State: closed - Opened by maximedenes over 4 years ago - 1 comment

#73 - Better names for dependencies

Issue - State: closed - Opened by lukaszcz over 4 years ago - 1 comment

#73 - Better names for dependencies

Issue - State: closed - Opened by lukaszcz over 4 years ago - 1 comment

#72 - README update to advertise standalone tactics more

Pull Request - State: closed - Opened by palmskog over 4 years ago

#72 - README update to advertise standalone tactics more

Pull Request - State: closed - Opened by palmskog over 4 years ago

#71 - Branch for Coq 8.12

Issue - State: closed - Opened by palmskog over 4 years ago - 2 comments

#71 - Branch for Coq 8.12

Issue - State: closed - Opened by palmskog over 4 years ago - 2 comments

#70 - Failing hammer tactic causes Coq anomaly in Coq 8.11

Issue - State: closed - Opened by palmskog over 4 years ago - 4 comments

#70 - Failing hammer tactic causes Coq anomaly in Coq 8.11

Issue - State: closed - Opened by palmskog over 4 years ago - 4 comments

#69 - Add all old tactics from Hammer.Reconstr as the third reconstruction batch.

Issue - State: closed - Opened by lukaszcz over 4 years ago - 1 comment
Labels: enhancement

#69 - Add all old tactics from Hammer.Reconstr as the third reconstruction batch.

Issue - State: closed - Opened by lukaszcz over 4 years ago - 1 comment
Labels: enhancement

#68 - Hint databases in sauto

Issue - State: closed - Opened by lukaszcz over 4 years ago - 1 comment
Labels: enhancement

#68 - Hint databases in sauto

Issue - State: closed - Opened by lukaszcz over 4 years ago - 1 comment
Labels: enhancement

#67 - Missing application and inversion actions in sauto

Issue - State: closed - Opened by lukaszcz over 4 years ago - 1 comment
Labels: bug

#67 - Missing application and inversion actions in sauto

Issue - State: closed - Opened by lukaszcz over 4 years ago - 1 comment
Labels: bug

#66 - Adapt to change of search API (Coq PR #8855).

Pull Request - State: closed - Opened by Zimmi48 almost 5 years ago - 1 comment

#66 - Adapt to change of search API (Coq PR #8855).

Pull Request - State: closed - Opened by Zimmi48 almost 5 years ago - 1 comment

#65 - Dependency prediction failure in CoqIDE on MacOS

Issue - State: closed - Opened by lukaszcz almost 5 years ago - 1 comment
Labels: bug

#65 - Dependency prediction failure in CoqIDE on MacOS

Issue - State: closed - Opened by lukaszcz almost 5 years ago - 1 comment
Labels: bug

#64 - "Anomaly: Not_found" with parallel proof processing in CoqIDE

Issue - State: closed - Opened by Zhang-Liao almost 5 years ago - 5 comments
Labels: bug

#64 - "Anomaly: Not_found" with parallel proof processing in CoqIDE

Issue - State: closed - Opened by Zhang-Liao almost 5 years ago - 5 comments
Labels: bug

#63 - Fix compilation on coq master.

Pull Request - State: closed - Opened by ppedrot almost 5 years ago

#63 - Fix compilation on coq master.

Pull Request - State: closed - Opened by ppedrot almost 5 years ago

#62 - 8.11 + extraction

Issue - State: closed - Opened by llelf almost 5 years ago - 1 comment

#62 - 8.11 + extraction

Issue - State: closed - Opened by llelf almost 5 years ago - 1 comment

#61 - fix getopt invocation

Pull Request - State: closed - Opened by llelf almost 5 years ago

#61 - fix getopt invocation

Pull Request - State: closed - Opened by llelf almost 5 years ago

#60 - Is it able to set the number of predicted premises returned by tactic "predict"?

Issue - State: closed - Opened by Zhang-Liao almost 5 years ago - 1 comment

#60 - Is it able to set the number of predicted premises returned by tactic "predict"?

Issue - State: closed - Opened by Zhang-Liao almost 5 years ago - 1 comment

#59 - Fix w.r.t. coq/coq#11896.

Pull Request - State: closed - Opened by ppedrot almost 5 years ago - 1 comment

#58 - Hosting historical CoqHammer archives on GitHub

Issue - State: closed - Opened by palmskog almost 5 years ago - 2 comments

#58 - Hosting historical CoqHammer archives on GitHub

Issue - State: closed - Opened by palmskog almost 5 years ago - 2 comments

#57 - OPAM fixes for 8.11

Pull Request - State: closed - Opened by palmskog almost 5 years ago

#57 - OPAM fixes for 8.11

Pull Request - State: closed - Opened by palmskog almost 5 years ago

#56 - OPAM fixes for 8.10

Pull Request - State: closed - Opened by palmskog almost 5 years ago

#56 - OPAM fixes for 8.10

Pull Request - State: closed - Opened by palmskog almost 5 years ago

#55 - Adapt to coq/coq#11521 (remove Goptions.optname field)

Pull Request - State: closed - Opened by SkySkimmer about 5 years ago - 1 comment

#55 - Adapt to coq/coq#11521 (remove Goptions.optname field)

Pull Request - State: closed - Opened by SkySkimmer about 5 years ago - 1 comment

#54 - Revert "Adapt to coq/coq#11521 (remove Goptions.optname field)"

Pull Request - State: closed - Opened by lukaszcz about 5 years ago

#54 - Revert "Adapt to coq/coq#11521 (remove Goptions.optname field)"

Pull Request - State: closed - Opened by lukaszcz about 5 years ago

#53 - Use coqhammer for a user changed coq

Issue - State: closed - Opened by Zhang-Liao about 5 years ago - 4 comments

GitHub / lukaszcz/coqhammer issues and pull requests