Ecosyste.ms: Issues

An open API service for providing issue and pull request metadata for open source projects.

GitHub / coq-tactician/coq-tactician issues and pull requests

#92 - Adapt w.r.t. coq/coq#19743.

Pull Request - State: closed - Opened by ppedrot about 1 month ago - 1 comment

#91 - Adapt w.r.t. coq/coq#19736.

Pull Request - State: closed - Opened by ppedrot about 1 month ago - 1 comment

#90 - Adapt to coq/coq#19646 (wit_constr_context doesn't exist anymore)

Pull Request - State: closed - Opened by SkySkimmer about 2 months ago - 1 comment

#89 - Adapt w.r.t. coq/coq#19481.

Pull Request - State: closed - Opened by ppedrot 3 months ago - 1 comment

#88 - Fast namegen detyping

Pull Request - State: closed - Opened by ppedrot 3 months ago

#86 - Adapt w.r.t. coq/coq#19313.

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

#85 - adapt to coq/coq#19147

Pull Request - State: closed - Opened by gares 5 months ago - 1 comment

#84 - [coq] Adapt to coq/coq#19124

Pull Request - State: closed - Opened by ejgallego 6 months ago - 5 comments

#83 - Adapt to coq/coq#18973.

Pull Request - State: closed - Opened by rlepigre 6 months ago - 1 comment

#82 - Remove legacy build mode

Pull Request - State: closed - Opened by ejgallego 7 months ago - 1 comment

#81 - Adapt to coq/coq#18938 (EConstr.ERelevance)

Pull Request - State: closed - Opened by SkySkimmer 8 months ago - 1 comment

#80 - Adapt w.r.t. coq/coq#18852

Pull Request - State: closed - Opened by LasseBlaauwbroek 8 months ago - 1 comment

#79 - Adapt w.r.t. coq/coq#18666.

Pull Request - State: closed - Opened by ppedrot 10 months ago - 3 comments

#78 - Adapt to coq/coq#18038 (rewrite rules)

Pull Request - State: closed - Opened by yannl35133 10 months ago - 1 comment

#77 - Adapt to coq/coq#18529 (no Dyn.anonymous)

Pull Request - State: closed - Opened by SkySkimmer 10 months ago - 1 comment

#76 - Adapt to coq/coq#18528 (toplevel_selector moved to G_vernac)

Pull Request - State: closed - Opened by SkySkimmer 10 months ago - 1 comment

#75 - Adapt to coq/coq#18352 (ltacX_common_plugin)

Pull Request - State: closed - Opened by SkySkimmer 11 months ago - 1 comment

#74 - Adapt to coq/coq#18094: rewrite strategies: fix

Pull Request - State: closed - Opened by JasonGross 11 months ago - 2 comments

#73 - Adapt to coq/coq#18143 (debug printing for relevances)

Pull Request - State: closed - Opened by SkySkimmer 12 months ago - 1 comment

#73 - Adapt to coq/coq#18143 (debug printing for relevances)

Pull Request - State: closed - Opened by SkySkimmer 12 months ago - 1 comment

#72 - Adapt to coq/coq#18327 (projection opacity)

Pull Request - State: closed - Opened by rlepigre 12 months ago - 1 comment

#71 - Centralize use of Stm

Pull Request - State: closed - Opened by SkySkimmer 12 months ago - 6 comments

#70 - Adapt w.r.t. coq/coq#18294.

Pull Request - State: closed - Opened by ppedrot about 1 year ago - 1 comment

#69 - Adapt to coq/coq#18280 (case relevance outside case info)

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

#68 - Adapt to https://github.com/coq/coq/pull/14928

Pull Request - State: closed - Opened by proux01 about 1 year ago - 1 comment

#67 - Adapt w.r.t. coq/coq#18124 (Remove the TacComplete AST)

Pull Request - State: closed - Opened by LasseBlaauwbroek about 1 year ago - 1 comment

#66 - Adapt to coq/coq#17667 (quotations in patterns)

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

#65 - Adapt to coq/coq#17836 (sort poly)

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

#64 - Adapt to coq/coq#17818 (APIs moved to `Vernactypes`)

Pull Request - State: closed - Opened by SkySkimmer over 1 year ago - 1 comment

#63 - Adapt to coq/coq#17664 (goptions use Deprecation.t option instead of bool)

Pull Request - State: closed - Opened by SkySkimmer over 1 year ago - 1 comment

#62 - Adapt to coq/coq#17331 (parsing separation)

Pull Request - State: closed - Opened by SkySkimmer over 1 year ago - 2 comments

#61 - Explicitly depend on stm

Pull Request - State: closed - Opened by SkySkimmer over 1 year ago - 1 comment

#60 - Adapt to Coq PR #17115

Pull Request - State: closed - Opened by herbelin over 1 year ago - 6 comments

#59 - Limit the depth of proof search

Issue - State: open - Opened by Zhang-Liao over 2 years ago - 5 comments

#58 - Don't backtrack into solved branches

Issue - State: closed - Opened by LasseBlaauwbroek almost 3 years ago - 1 comment
Labels: next-release

#57 - merge coq8.11 to negative-local-context

Pull Request - State: closed - Opened by Zhang-Liao almost 3 years ago

#56 - Fast features

Pull Request - State: closed - Opened by LasseBlaauwbroek almost 3 years ago - 3 comments

#55 - Debug benchmark crashes on >= 8.14

Issue - State: closed - Opened by LasseBlaauwbroek almost 3 years ago - 1 comment
Labels: next-release

#54 - Tune the timeout of tactics during proof synthesis

Issue - State: open - Opened by LasseBlaauwbroek almost 3 years ago

#53 - Feature ideas

Issue - State: open - Opened by LasseBlaauwbroek almost 3 years ago - 5 comments

#52 - Canonicalize terms w.r.t. kernel names in the feature generation function

Issue - State: closed - Opened by LasseBlaauwbroek almost 3 years ago - 1 comment
Labels: next-release

#51 - Consider given the feature vectors a maximum length

Issue - State: open - Opened by LasseBlaauwbroek almost 3 years ago
Labels: next-release

#50 - See if it is possible to not save non-canonical objects in compiled binaries

Issue - State: open - Opened by LasseBlaauwbroek almost 3 years ago
Labels: next-release

#49 - reverse map to avoid stack flow

Pull Request - State: closed - Opened by Zhang-Liao almost 3 years ago

#48 - Remove most bash scripts in tactician exec

Pull Request - State: closed - Opened by LasseBlaauwbroek almost 3 years ago

#47 - Subst patch

Pull Request - State: closed - Opened by pestun almost 3 years ago - 1 comment

#46 - xargs to strip new lines from cat of injection-flags

Pull Request - State: closed - Opened by pestun almost 3 years ago - 1 comment

#45 - Error installing coq-tactician-stdlib

Issue - State: closed - Opened by sgodwincs almost 3 years ago - 2 comments

#44 - Upgrade Opam dependency to 2.1.0

Issue - State: closed - Opened by LasseBlaauwbroek over 3 years ago
Labels: next-release

#43 - Rename `search`

Issue - State: closed - Opened by LasseBlaauwbroek over 3 years ago
Labels: next-release

#42 - Add decomposition support for ssreflect

Issue - State: open - Opened by LasseBlaauwbroek over 3 years ago

#41 - Better windows support

Issue - State: open - Opened by LasseBlaauwbroek over 3 years ago

#40 - Optimize decomposition settings

Issue - State: open - Opened by LasseBlaauwbroek over 3 years ago

#38 - Properly decompose intropatterns

Issue - State: open - Opened by LasseBlaauwbroek over 3 years ago

#36 - Deal better with dependent goals

Issue - State: open - Opened by LasseBlaauwbroek over 3 years ago

#35 - Finish rebuilding whole `outcome`

Issue - State: open - Opened by LasseBlaauwbroek over 3 years ago

#34 - Make Tactician's datastructures more lazy

Issue - State: open - Opened by LasseBlaauwbroek over 3 years ago

#33 - Fix `userPredict` population of `outcome`

Issue - State: open - Opened by LasseBlaauwbroek over 3 years ago

#32 - Optimize the feature generation function

Issue - State: open - Opened by LasseBlaauwbroek over 3 years ago - 1 comment

#30 - Better factoring of the search procedure

Issue - State: open - Opened by LasseBlaauwbroek over 3 years ago

#29 - Improve the predictions of variables pointing to the local context

Issue - State: open - Opened by LasseBlaauwbroek over 3 years ago
Labels: model-idea

#28 - Take a look at how section discharging works with proof states

Issue - State: open - Opened by LasseBlaauwbroek over 3 years ago - 1 comment

#26 - Integrate CoqHammer's `sauto` with lemma prediction

Issue - State: open - Opened by LasseBlaauwbroek over 3 years ago
Labels: model-idea

#25 - Record the tactics produced by 'search'

Issue - State: open - Opened by LasseBlaauwbroek over 3 years ago

#24 - Consider creating a model that employs `iauto`

Issue - State: open - Opened by LasseBlaauwbroek over 3 years ago
Labels: model-idea

#23 - "Streamify" the LSHF learner

Issue - State: open - Opened by LasseBlaauwbroek over 3 years ago
Labels: next-release

#22 - Inline discharged `Let` definitions into tactics when needed.

Issue - State: open - Opened by LasseBlaauwbroek over 3 years ago
Labels: next-release

#21 - Fix alpha conversion for section discharging

Issue - State: open - Opened by LasseBlaauwbroek over 3 years ago
Labels: next-release

#20 - Make `tactician` utility deal better with package removal

Issue - State: open - Opened by LasseBlaauwbroek over 3 years ago
Labels: next-release

#19 - Move the `tactician_ignore`, `admit`, `search` and `search with cache` check to `Tactic_annotate`

Issue - State: open - Opened by LasseBlaauwbroek over 3 years ago - 1 comment
Labels: next-release

#18 - Make `Suggest` async

Issue - State: open - Opened by LasseBlaauwbroek over 3 years ago
Labels: next-release

#16 - Implement MinHashing with single hash function

Issue - State: open - Opened by LasseBlaauwbroek over 3 years ago
Labels: next-release

#15 - Adapt our code the upstream changes making `cpattern` and `rpattern` accessible

Issue - State: closed - Opened by LasseBlaauwbroek over 3 years ago
Labels: next-release

#14 - Make tactic recording not use `TacThen (run_pushs_state_tac (), TacThen (tac, run_record_tac orig))`

Issue - State: closed - Opened by LasseBlaauwbroek over 3 years ago - 1 comment
Labels: next-release

#12 - Only depend onto `coq-core` instead of `coq`

Issue - State: closed - Opened by LasseBlaauwbroek over 3 years ago
Labels: next-release

#11 - Benchmarking: Check the generated proof witness

Issue - State: open - Opened by LasseBlaauwbroek over 3 years ago

#10 - Discard tactics marked as unsafe

Issue - State: open - Opened by LasseBlaauwbroek over 3 years ago
Labels: next-release

#9 - Tactician utility: Only recompile packages that do not depend on `coq-tactician`

Issue - State: open - Opened by LasseBlaauwbroek over 3 years ago
Labels: next-release

#8 - Debug slowdown of imports between beta1 and now

Issue - State: closed - Opened by LasseBlaauwbroek over 3 years ago - 1 comment
Labels: next-release

#6 - fix features out of memory

Pull Request - State: closed - Opened by Zhang-Liao over 3 years ago - 3 comments

#5 - Coq8.11 features

Pull Request - State: closed - Opened by Zhang-Liao almost 4 years ago - 3 comments

#4 - Coq8.11 features

Pull Request - State: closed - Opened by Zhang-Liao almost 4 years ago - 1 comment

#3 - Fix discharging of tactic notations

Pull Request - State: closed - Opened by LasseBlaauwbroek almost 4 years ago

#2 - macOS support (bwrap)

Issue - State: closed - Opened by anton-trunov almost 4 years ago - 19 comments

#1 - please support Fail

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