PUMPKIN-PATCH icon indicating copy to clipboard operation
PUMPKIN-PATCH copied to clipboard

Published 20 hours ago • verified publisher icon uwplse
→

Metadata

Proof Updater Mechanically Passing Knowledge Into New Proofs, Assisting The Coq Hacker

Results 45 PUMPKIN-PATCH issues
Sort by recently updated
recently updated
newest added

Decompiler Test Suite

Decompiler needs lots of regression tests. Plan: * .v full of terms * decompile command to print decompiled tactics to console * ground truth file to diff with

randair avatar randair

.mli for decompiler.ml module

decompiler.ml needs a .mli file so only certain functions are exposed.

randair avatar randair

enhancement

What should the UI for refactoring be?

Here's one answer/vote: I think the UI for issuing refactoring commands should be just the language server protocol (https://langserver.org/), like this all editors supporting the protocol will be able to...

samuelgruetter avatar samuelgruetter

wish
UI

Adding new constructors/cases

tlringer avatar tlringer

Use Constrintern.interp_constr_evars over Constrintern.interp_constr (globally)

tlringer avatar tlringer

Optimization.v bugs

tlringer avatar tlringer

Rerun all tests and eval for both PUMPKIN PATCH and DEVOID

10 comment

tlringer avatar tlringer

blocked

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

tlringer avatar tlringer

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

tlringer avatar tlringer

Better type hygiene (globally)

https://github.com/coq/coq/blob/master/doc/plugin_tutorial/tuto1/src/simple_check.ml

tlringer avatar tlringer

meta

← Metadata

50
Stars
2
Forks
Watchers

Owner

verified publisher icon uwplse

Metadata

Proof Updater Mechanically Passing Knowledge Into New Proofs, Assisting The Coq Hacker

Back