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 22 days ago
- 1 comment
#91 - Adapt w.r.t. coq/coq#19736.
Pull Request -
State: closed - Opened by ppedrot 22 days ago
- 1 comment
#90 - Adapt to coq/coq#19646 (wit_constr_context doesn't exist anymore)
Pull Request -
State: closed - Opened by SkySkimmer about 1 month 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
#87 - Adapt to Coq PR #19404: an algebra of types for the instances of notation variables
Pull Request -
State: open - Opened by herbelin 4 months ago
#86 - Adapt w.r.t. coq/coq#19313.
Pull Request -
State: closed - Opened by ppedrot 4 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 5 months ago
- 5 comments
#83 - Adapt to coq/coq#18973.
Pull Request -
State: closed - Opened by rlepigre 5 months ago
- 1 comment
#82 - Remove legacy build mode
Pull Request -
State: closed - Opened by ejgallego 6 months ago
- 1 comment
#81 - Adapt to coq/coq#18938 (EConstr.ERelevance)
Pull Request -
State: closed - Opened by SkySkimmer 7 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 9 months ago
- 3 comments
#78 - Adapt to coq/coq#18038 (rewrite rules)
Pull Request -
State: closed - Opened by yannl35133 9 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 10 months ago
- 1 comment
#74 - Adapt to coq/coq#18094: rewrite strategies: fix
Pull Request -
State: closed - Opened by JasonGross 10 months ago
- 2 comments
#73 - Adapt to coq/coq#18143 (debug printing for relevances)
Pull Request -
State: closed - Opened by SkySkimmer 11 months ago
- 1 comment
#73 - Adapt to coq/coq#18143 (debug printing for relevances)
Pull Request -
State: closed - Opened by SkySkimmer 11 months ago
- 1 comment
#72 - Adapt to coq/coq#18327 (projection opacity)
Pull Request -
State: closed - Opened by rlepigre 11 months ago
- 1 comment
#71 - Centralize use of Stm
Pull Request -
State: closed - Opened by SkySkimmer 11 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 about 3 years ago
Labels: next-release
#43 - Rename `search`
Issue -
State: closed - Opened by LasseBlaauwbroek about 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
#39 - Implement efficient reconstruction procedure for `search with cache` failures
Issue -
State: open - Opened by LasseBlaauwbroek over 3 years ago
#38 - Properly decompose intropatterns
Issue -
State: open - Opened by LasseBlaauwbroek over 3 years ago
#37 - Use the tactic mapping monad for decomposition functions
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
#31 - Implement proper hash-consing for tactic expressions
Issue -
State: open - Opened by LasseBlaauwbroek over 3 years ago
#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
#27 - Remove the timeout fork hack, will require all errors to be resolved
Issue -
State: open - Opened by LasseBlaauwbroek over 3 years ago
#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
#13 - Change 'with-tactician' to have the correct paths substituted in, instead of querying opam on every call
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
#7 - Return `glob_tactic_expr tactic` instead of `glob_tactic_expr stream` from model prediction
Issue -
State: open - Opened by LasseBlaauwbroek over 3 years ago
#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 over 3 years ago
- 3 comments
#4 - Coq8.11 features
Pull Request -
State: closed - Opened by Zhang-Liao over 3 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