uwplse/PUMPKIN-PATCH issues and pull requests

#86 - Update .gitmodules to use 8.9

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

#86 - Update .gitmodules to use 8.9

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

#85 - New hint interface.

Pull Request - State: closed - Opened by Radnyx over 3 years ago

#85 - New hint interface.

Pull Request - State: closed - Opened by Radnyx over 3 years ago

#84 - Moved parse_tac_str.

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

#84 - Moved parse_tac_str.

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

#83 - + Collapse intro/revert.+ Pass in custom tactics.

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

#83 - + Collapse intro/revert.+ Pass in custom tactics.

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

#82 - Shallow semicolons.

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

#82 - Shallow semicolons.

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

#81 - Better induction /// exists for existT

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

#81 - Better induction /// exists for existT

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

#80 - Many things

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

#80 - Many things

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

#79 - Induction

Pull Request - State: closed - Opened by randair over 4 years ago - 2 comments

#79 - Induction

Pull Request - State: closed - Opened by randair over 4 years ago - 2 comments

#78 - apply-in/pose

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

#78 - apply-in/pose

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

#77 - Left, right, split.

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

#77 - Left, right, split.

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

#76 - Regression test script for decompiler.

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

#76 - Regression test script for decompiler.

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

#75 - Rewrite-In hypothesis transformation.

Pull Request - State: closed - Opened by randair almost 5 years ago - 2 comments

#75 - Rewrite-In hypothesis transformation.

Pull Request - State: closed - Opened by randair almost 5 years ago - 2 comments

#74 - Decompiler Test Suite

Issue - State: open - Opened by randair almost 5 years ago

#74 - Decompiler Test Suite

Issue - State: open - Opened by randair almost 5 years ago

#73 - Simple rewrite tactic decompilation

Pull Request - State: closed - Opened by randair almost 5 years ago - 2 comments

#73 - Simple rewrite tactic decompilation

Pull Request - State: closed - Opened by randair almost 5 years ago - 2 comments

#72 - .mli for decompiler.ml module

Issue - State: open - Opened by randair almost 5 years ago
Labels: enhancement

#72 - .mli for decompiler.ml module

Issue - State: open - Opened by randair almost 5 years ago
Labels: enhancement

#71 - Decompile coq terms into tactic list.

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

#71 - Decompile coq terms into tactic list.

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

#70 - Suggest patch tactic

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

#70 - Suggest patch tactic

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

#69 - patch/as tactic

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

#69 - patch/as tactic

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

#68 - What should the UI for refactoring be?

Issue - State: open - Opened by samuelgruetter about 5 years ago
Labels: wish, UI

#68 - What should the UI for refactoring be?

Issue - State: open - Opened by samuelgruetter about 5 years ago
Labels: wish, UI

#67 - Adding new constructors/cases

Issue - State: open - Opened by tlringer about 5 years ago

#66 - Use Constrintern.interp_constr_evars over Constrintern.interp_constr (globally)

Issue - State: open - Opened by tlringer about 5 years ago

#66 - Use Constrintern.interp_constr_evars over Constrintern.interp_constr (globally)

Issue - State: open - Opened by tlringer about 5 years ago

#65 - Optimization.v bugs

Issue - State: open - Opened by tlringer about 5 years ago

#65 - Optimization.v bugs

Issue - State: open - Opened by tlringer about 5 years ago

#64 - 0.1 release

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

#64 - 0.1 release

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

#63 - Investigate which reductions, evar_maps, and so on are admissible for performance gains (globally)

Issue - State: open - Opened by tlringer over 5 years ago

#63 - Investigate which reductions, evar_maps, and so on are admissible for performance gains (globally)

Issue - State: open - Opened by tlringer over 5 years ago

#62 - use built-in coq functions wherever possible (at lib level, at least) (investigate globally)

Issue - State: open - Opened by tlringer over 5 years ago

#62 - use built-in coq functions wherever possible (at lib level, at least) (investigate globally)

Issue - State: open - Opened by tlringer over 5 years ago

#61 - Move stateless reducers (e.g., reduce_stateless reduce_term) and other common functions back into lib (globally)

Issue - State: closed - Opened by tlringer over 5 years ago

#61 - Move stateless reducers (e.g., reduce_stateless reduce_term) and other common functions back into lib (globally)

Issue - State: closed - Opened by tlringer over 5 years ago

#60 - Better type hygiene (globally)

Issue - State: open - Opened by tlringer over 5 years ago
Labels: meta

#60 - Better type hygiene (globally)

Issue - State: open - Opened by tlringer over 5 years ago
Labels: meta

#59 - Go back to tactics: basic version (cut lemma)

Issue - State: open - Opened by tlringer over 5 years ago

#59 - Go back to tactics: basic version (cut lemma)

Issue - State: open - Opened by tlringer over 5 years ago

#58 - Determine common refactorings to support from the Analytics project

Issue - State: open - Opened by tlringer over 5 years ago
Labels: blocked, meta

#58 - Determine common refactorings to support from the Analytics project

Issue - State: open - Opened by tlringer over 5 years ago
Labels: blocked, meta

#57 - Renaming definitions

Issue - State: open - Opened by tlringer over 5 years ago

#57 - Renaming definitions

Issue - State: open - Opened by tlringer over 5 years ago

#56 - Renaming constructors

Issue - State: open - Opened by tlringer over 5 years ago

#56 - Renaming constructors

Issue - State: open - Opened by tlringer over 5 years ago

#55 - Renaming hypotheses

Issue - State: open - Opened by tlringer over 5 years ago

#55 - Renaming hypotheses

Issue - State: open - Opened by tlringer over 5 years ago

#54 - Moving definitions between files/modules

Issue - State: open - Opened by tlringer over 5 years ago

#54 - Moving definitions between files/modules

Issue - State: open - Opened by tlringer over 5 years ago

#53 - Reducio integration from the magic plugin

Issue - State: open - Opened by tlringer over 5 years ago

#53 - Reducio integration from the magic plugin

Issue - State: open - Opened by tlringer over 5 years ago

#52 - File organization

Issue - State: open - Opened by tlringer over 5 years ago

#52 - File organization

Issue - State: open - Opened by tlringer over 5 years ago

#51 - Move TODOs to issues (globally)

Issue - State: open - Opened by tlringer over 5 years ago
Labels: meta

#51 - Move TODOs to issues (globally)

Issue - State: open - Opened by tlringer over 5 years ago
Labels: meta

#50 - Move TODOs to issues (global)

Issue - State: open - Opened by tlringer over 5 years ago

#50 - Move TODOs to issues (global)

Issue - State: open - Opened by tlringer over 5 years ago

#49 - Examples of PUMPKIN PATCH & DEVOID together!

Issue - State: open - Opened by tlringer over 5 years ago

#48 - Rename components (everywhere) to avoid name collisions

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

#47 - Move coq-plugin-lib to deps (everywhere)

Issue - State: closed - Opened by tlringer over 5 years ago

#46 - Make it Pumpkin.Patch instead of Patcher.Patch

Issue - State: closed - Opened by tlringer over 5 years ago

#45 - Manage permissions of all of the repos

Issue - State: open - Opened by tlringer over 5 years ago

#44 - Much better build process (actual dependencies instead of submodules, which were just for development purposes)

Issue - State: open - Opened by tlringer over 5 years ago - 1 comment

#43 - Refactor code that has to do with relating two terms or contexts (DEVOID, PUMPKIN, and libs)

Issue - State: closed - Opened by tlringer over 5 years ago
Labels: meta

#42 - Rerun all tests and eval for both PUMPKIN PATCH and DEVOID

Issue - State: open - Opened by tlringer over 5 years ago - 10 comments
Labels: blocked

#41 - Name collision with reverse

Issue - State: closed - Opened by tlringer over 5 years ago

#40 - Use twice and reverse in PUMPKIN PATCH

Issue - State: closed - Opened by tlringer over 5 years ago

#39 - Consider refactoring components, too

Issue - State: open - Opened by tlringer over 5 years ago
Labels: meta

#38 - Post-category-removal: move more functions into lib

Issue - State: open - Opened by tlringer over 5 years ago
Labels: blocked

#37 - Better representation for cut lemmas

Issue - State: open - Opened by tlringer over 5 years ago

#36 - Clean up or move merging

Issue - State: open - Opened by tlringer over 5 years ago

#35 - Better representation for candidates

Issue - State: open - Opened by tlringer over 5 years ago

#34 - Better representation for assumptions

Issue - State: open - Opened by tlringer over 5 years ago

#33 - Merge into master

Issue - State: closed - Opened by tlringer over 5 years ago

#32 - Release

Issue - State: closed - Opened by tlringer over 5 years ago

#31 - Update docs

Issue - State: closed - Opened by tlringer over 5 years ago

#30 - Depend on DEVOID core after refactoring

Issue - State: closed - Opened by tlringer over 5 years ago

#28 - Refactor Fixpoint to eliminator translation (common to DEVOID and PUMPKIN PATCH)

Issue - State: closed - Opened by tlringer over 5 years ago

#27 - Refactor Coq plugin library (common to DEVOID and PUMPKIN PATCH)

Issue - State: closed - Opened by tlringer over 5 years ago

#26 - Add a build script

Issue - State: closed - Opened by tlringer over 5 years ago

#25 - Remove explicit category theory references

Issue - State: open - Opened by tlringer over 5 years ago

#24 - Library organization

Issue - State: closed - Opened by tlringer over 5 years ago - 2 comments
Labels: meta

#23 - Basic Proof Optimization (fixes #6)

Pull Request - State: closed - Opened by tlringer over 5 years ago

#22 - If Optimize fails to find a faster proof, then fail.

Issue - State: open - Opened by tlringer over 5 years ago
Labels: enhancement

GitHub / uwplse/PUMPKIN-PATCH issues and pull requests