uwplse/PUMPKIN-PATCH issues and pull requests

#86 - Update .gitmodules to use 8.9

Pull Request - State: open - Opened by agrarpan about 1 year ago

#85 - New hint interface.

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

#84 - Moved parse_tac_str.

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

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

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

#82 - Shallow semicolons.

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

#81 - Better induction /// exists for existT

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

#80 - Many things

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

#79 - Induction

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

#78 - apply-in/pose

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

#77 - Left, right, split.

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

#76 - Regression test script for decompiler.

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

#75 - Rewrite-In hypothesis transformation.

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

#74 - Decompiler Test Suite

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

#73 - Simple rewrite tactic decompilation

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

#72 - .mli for decompiler.ml module

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

#71 - Decompile coq terms into tactic list.

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

#70 - Suggest patch tactic

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

#69 - patch/as tactic

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

#68 - What should the UI for refactoring be?

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

#67 - Adding new constructors/cases

Issue - State: open - Opened by tlringer almost 6 years ago

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

Issue - State: open - Opened by tlringer almost 6 years ago

#65 - Optimization.v bugs

Issue - State: open - Opened by tlringer almost 6 years ago

#64 - 0.1 release

Pull Request - State: closed - Opened by tlringer almost 6 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 almost 6 years ago

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

Issue - State: open - Opened by tlringer almost 6 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 almost 6 years ago

#60 - Better type hygiene (globally)

Issue - State: open - Opened by tlringer almost 6 years ago
Labels: meta

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

Issue - State: open - Opened by tlringer almost 6 years ago

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

Issue - State: open - Opened by tlringer almost 6 years ago
Labels: blocked, meta

#57 - Renaming definitions

Issue - State: open - Opened by tlringer almost 6 years ago

#56 - Renaming constructors

Issue - State: open - Opened by tlringer almost 6 years ago

#55 - Renaming hypotheses

Issue - State: open - Opened by tlringer almost 6 years ago

#54 - Moving definitions between files/modules

Issue - State: open - Opened by tlringer almost 6 years ago

#53 - Reducio integration from the magic plugin

Issue - State: open - Opened by tlringer almost 6 years ago

#52 - File organization

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

#51 - Move TODOs to issues (globally)

Issue - State: open - Opened by tlringer about 6 years ago
Labels: meta

#50 - Move TODOs to issues (global)

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

#49 - Examples of PUMPKIN PATCH & DEVOID together!

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

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

Issue - State: open - Opened by tlringer about 6 years ago - 2 comments

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

Issue - State: closed - Opened by tlringer about 6 years ago

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

Issue - State: closed - Opened by tlringer about 6 years ago

#45 - Manage permissions of all of the repos

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

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

Issue - State: open - Opened by tlringer about 6 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 about 6 years ago
Labels: meta

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

Issue - State: open - Opened by tlringer about 6 years ago - 10 comments
Labels: blocked

#41 - Name collision with reverse

Issue - State: closed - Opened by tlringer about 6 years ago

#40 - Use twice and reverse in PUMPKIN PATCH

Issue - State: closed - Opened by tlringer about 6 years ago

#39 - Consider refactoring components, too

Issue - State: open - Opened by tlringer about 6 years ago
Labels: meta

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

Issue - State: open - Opened by tlringer about 6 years ago
Labels: blocked

#37 - Better representation for cut lemmas

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

#36 - Clean up or move merging

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

#35 - Better representation for candidates

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

#34 - Better representation for assumptions

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

#33 - Merge into master

Issue - State: closed - Opened by tlringer about 6 years ago

#32 - Release

Issue - State: closed - Opened by tlringer about 6 years ago

#31 - Update docs

Issue - State: closed - Opened by tlringer about 6 years ago

#30 - Depend on DEVOID core after refactoring

Issue - State: closed - Opened by tlringer about 6 years ago

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

Issue - State: closed - Opened by tlringer about 6 years ago

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

Issue - State: closed - Opened by tlringer about 6 years ago

#26 - Add a build script

Issue - State: closed - Opened by tlringer about 6 years ago

#25 - Remove explicit category theory references

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

#24 - Library organization

Issue - State: closed - Opened by tlringer about 6 years ago - 2 comments
Labels: meta

#23 - Basic Proof Optimization (fixes #6)

Pull Request - State: closed - Opened by tlringer about 6 years ago

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

Issue - State: open - Opened by tlringer about 6 years ago
Labels: enhancement

#21 - See if it is possible to extend proof optimization to also optimize functions

Issue - State: open - Opened by tlringer about 6 years ago
Labels: enhancement, question

#20 - Does proof patching work well with trees?

Issue - State: open - Opened by tlringer about 6 years ago
Labels: question

#19 - Add support for cutting lemmas in optimization

Issue - State: open - Opened by tlringer about 6 years ago
Labels: enhancement

#18 - Implement good nested induction support

Issue - State: open - Opened by tlringer about 6 years ago
Labels: enhancement

#17 - PUMPKIN PATCH is bad at understanding rewrites

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

#16 - Inductive hypotheses in _rect eliminators aren't recognized as inductive hypotheses

Issue - State: open - Opened by tlringer about 6 years ago - 2 comments
Labels: bug, blocked

#15 - Failure case patch is not quite what we want

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

#14 - PUMPKIN isn't smart enough for patching eliminators of different sorts yet

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

#13 - Merge Nate's fixpoint to induction principle translation in from DEVOID (fixes #5)

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

#12 - Run Preprocess automatically

Issue - State: open - Opened by tlringer about 6 years ago - 1 comment

#11 - Put into the Coq CI

Issue - State: open - Opened by tlringer about 6 years ago
Labels: blocked

#10 - Update to latest coq version

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

#9 - Use good evar_map hygeine

Issue - State: closed - Opened by tlringer about 6 years ago - 1 comment

#8 - Clean up code a lot

Issue - State: open - Opened by tlringer about 6 years ago - 2 comments
Labels: meta

#7 - Merge in DEVOID

Issue - State: closed - Opened by tlringer about 6 years ago
Labels: meta

#6 - Implement proof optimization

Issue - State: closed - Opened by tlringer about 6 years ago
Labels: enhancement

#5 - Merge fixpoint to induction principle translation in from DEVOID

Issue - State: closed - Opened by tlringer about 6 years ago

#4 - Make a test script

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

#3 - Website

Pull Request - State: closed - Opened by nateyazdani over 7 years ago - 3 comments

#2 - Port to v8.6:

Pull Request - State: closed - Opened by ejgallego over 7 years ago - 5 comments
Labels: update

#1 - Refactor code to more closely match CPP paper

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

GitHub / uwplse/PUMPKIN-PATCH issues and pull requests