Ecosyste.ms: Issues
An open API service for providing issue and pull request metadata for open source projects.
GitHub / yforster/coq-verified-extraction issues and pull requests
#33 - Use released versions 1.3.2 of MetaCoq and 0.6 of malfunction and cor…
Pull Request -
State: closed - Opened by mattam82 3 months ago
#32 - Uncapitalize inductives & records
Pull Request -
State: closed - Opened by quimFIB 4 months ago
- 1 comment
#31 - Adapt reification to take into account extract inductive directives
Pull Request -
State: closed - Opened by mattam82 4 months ago
#30 - Reorder cstrs and unique ffi
Pull Request -
State: closed - Opened by mattam82 4 months ago
#29 - Cleanup the build process so that we don't need to install the ffi pl…
Pull Request -
State: closed - Opened by mattam82 5 months ago
#28 - Build fixes and doc
Pull Request -
State: closed - Opened by mattam82 5 months ago
- 1 comment
#27 - Question: Is it possible to compile the mlf files to OCaml bytecode, or to OCaml's Flambda IR?
Issue -
State: closed - Opened by mkarup 5 months ago
- 2 comments
#26 - Fix several things suggested by AE reviewers
Pull Request -
State: closed - Opened by yforster 8 months ago
#25 - Rename Malfunction.VerifiedPlugin.Loader into VerifiedExtraction.Extr…
Pull Request -
State: closed - Opened by yforster 8 months ago
#24 - Cleanup directory structure
Pull Request -
State: closed - Opened by yforster 8 months ago
#23 - Cleanup
Pull Request -
State: closed - Opened by yforster 8 months ago
#22 - Fix multiple function extraction
Pull Request -
State: closed - Opened by yforster 8 months ago
#21 - Rename "MetaCoq Extraction" to "Verified Extraction" everywhere
Pull Request -
State: closed - Opened by mattam82 8 months ago
#20 - Fix exports to not insert main as name
Pull Request -
State: closed - Opened by yforster 9 months ago
#19 - Update to latest metacoq (typo fix)
Pull Request -
State: closed - Opened by mattam82 9 months ago
#18 - Update metacoq commit
Pull Request -
State: closed - Opened by mattam82 9 months ago
#17 - Unsafe flags
Pull Request -
State: closed - Opened by mattam82 9 months ago
#16 - Support reification of computed results
Pull Request -
State: closed - Opened by mattam82 9 months ago
#15 - Fix and test bootstrapping and plugin feature (dynlink with coq)
Pull Request -
State: closed - Opened by mattam82 9 months ago
#14 - Extract inductive implementation
Pull Request -
State: closed - Opened by mattam82 9 months ago
#13 - Primarrays and compile fix
Pull Request -
State: closed - Opened by mattam82 9 months ago
#12 - Metacoq bump
Pull Request -
State: closed - Opened by mattam82 10 months ago
#11 - Missing "EPrimitive.prim_val" when building
Issue -
State: closed - Opened by quimFIB 10 months ago
- 1 comment
#10 - fix after update of EAst in Erasure
Pull Request -
State: closed - Opened by tabareau about 1 year ago
- 1 comment
#9 - complete pipeline up to admits
Pull Request -
State: closed - Opened by tabareau about 1 year ago
#8 - Enable benchmarking, and others things
Pull Request -
State: closed - Opened by yforster about 1 year ago
#7 - Verified plugin
Pull Request -
State: closed - Opened by mattam82 about 1 year ago
#6 - Pipeline theorem
Pull Request -
State: closed - Opened by yforster over 1 year ago
#5 - WIP on realizability semantics
Pull Request -
State: closed - Opened by tabareau over 1 year ago
#4 - complete proof that eval -> interpret
Pull Request -
State: closed - Opened by tabareau over 1 year ago
#3 - Make compatible with coq-ceres opam package
Pull Request -
State: closed - Opened by yforster over 1 year ago
#2 - semantics with heap
Pull Request -
State: closed - Opened by tabareau over 1 year ago
#1 - Extraction plugin
Pull Request -
State: closed - Opened by mattam82 about 2 years ago
- 1 comment