Ecosyste.ms: Issues

An open API service for providing issue and pull request metadata for open source projects.

GitHub / CertiCoq/certicoq issues and pull requests

#100 - Verified reordering cleanup

Pull Request - State: closed - Opened by mattam82 3 months ago

#99 - Fixes in prim_int63.c

Pull Request - State: closed - Opened by mattam82 4 months ago

#98 - Implement and verify the naive translation of lazy/force to thunks

Pull Request - State: closed - Opened by mattam82 5 months ago

#97 - Use new CI image avoiding opam updates

Pull Request - State: closed - Opened by yforster 6 months ago - 1 comment

#96 - Bugs in implementation of primitive operations

Issue - State: closed - Opened by mkarup 6 months ago - 9 comments

#95 - Coq 8.19 compatibility

Pull Request - State: closed - Opened by andrew-appel 8 months ago - 1 comment

#93 - Metacoq bump

Pull Request - State: closed - Opened by mattam82 9 months ago

#92 - Fix certicoq eval w.r.t. backtracking in Coq

Pull Request - State: closed - Opened by mattam82 9 months ago

#91 - We should test with gcc and compcert's ccomp

Issue - State: open - Opened by mattam82 9 months ago

#90 - Certicoq runtime / include cleanup

Pull Request - State: closed - Opened by mattam82 9 months ago

#88 - Certicoq Eval command and tactic

Pull Request - State: closed - Opened by mattam82 9 months ago

#87 - Fix deprecations

Pull Request - State: closed - Opened by mattam82 10 months ago

#86 - Define anf_trans using anf_state to help typeclass resolution

Pull Request - State: closed - Opened by Lysxia 10 months ago - 2 comments

#85 - Update metacoq

Pull Request - State: closed - Opened by mattam82 11 months ago - 2 comments

#84 - Change the `get_*_tag` glue function to return the right type of integer

Pull Request - State: closed - Opened by joom 11 months ago

#83 - Fixing absolute vs relative path in includes + some glue stuff

Pull Request - State: closed - Opened by joom 12 months ago

#82 - Get runtime after the latest CertiGraph changes

Pull Request - State: closed - Opened by joom 12 months ago

#81 - Differentiating including from path or library in the generated C code

Pull Request - State: closed - Opened by joom 12 months ago

#78 - Add `#pragma once` to all generated C files + other codegen and glue fixes

Pull Request - State: closed - Opened by joom 12 months ago - 1 comment

#77 - Fix type errors in generated glue

Pull Request - State: closed - Opened by joom about 1 year ago

#75 - Use a new CI image

Pull Request - State: closed - Opened by yforster about 1 year ago

#74 - Build fixes: certicoq and metacoq build scripts in coq 8.17.1

Pull Request - State: closed - Opened by andrew-appel about 1 year ago - 6 comments

#73 - ANF codegen should return values instead of putting them in args[1]

Pull Request - State: closed - Opened by joom about 1 year ago - 1 comment

#72 - Merging separate changes to 8.16 and 8.17

Pull Request - State: closed - Opened by joom about 1 year ago

#71 - Merge of my changes to the coq-8.15 branch

Pull Request - State: closed - Opened by joom about 1 year ago

#70 - Define value type in generated glue code

Pull Request - State: closed - Opened by joom over 1 year ago

#69 - Glue code: Remove separate argument accessor structs and functions

Pull Request - State: closed - Opened by joom over 1 year ago

#68 - Adjust glue code generator to ANF

Pull Request - State: closed - Opened by joom over 1 year ago

#67 - Coq 8.16 update

Pull Request - State: closed - Opened by mattam82 over 1 year ago

#66 - Changes in the 8.15 branch required by the VeriFFI project

Pull Request - State: closed - Opened by joom over 1 year ago

#65 - Version for Coq 8.17 (do not merge, just for CI)

Pull Request - State: closed - Opened by yforster over 1 year ago

#64 - correctness proof of Codegen doesn't compile

Issue - State: open - Opened by womeier over 1 year ago - 3 comments

#63 - function tags in LambdaANF are not unique

Issue - State: closed - Opened by womeier over 1 year ago - 2 comments

#62 - OPAM: requires Clang

Pull Request - State: closed - Opened by liyishuai over 1 year ago - 2 comments

#61 - ExtLib temporarily not tracking this project

Issue - State: closed - Opened by liyishuai over 1 year ago - 2 comments

#60 - Fix tinfo argument in prims, for CPS backend

Pull Request - State: closed - Opened by joom over 1 year ago

#59 - Remove the CertiCoq FFI command

Pull Request - State: closed - Opened by joom about 2 years ago

#58 - Renamings and cleanups

Pull Request - State: closed - Opened by mattam82 about 2 years ago

#57 - Certicoq register and run

Pull Request - State: closed - Opened by mattam82 about 2 years ago

#56 - `CertiCoq FFI` produces bad C code

Issue - State: open - Opened by kuruczgy about 2 years ago - 5 comments

#55 - Update to compcert 3.11 (using canonical maps)

Pull Request - State: closed - Opened by mattam82 over 2 years ago

#54 - Certicoq bootstrapped plugins

Pull Request - State: closed - Opened by mattam82 over 2 years ago

#53 - Performance improvements

Pull Request - State: closed - Opened by mattam82 over 2 years ago

#52 - Update CertiCoq to latest MetaCoq version

Pull Request - State: closed - Opened by mattam82 over 2 years ago

#51 - Inlined projections

Pull Request - State: closed - Opened by mattam82 over 2 years ago

#50 - Lbox To L2k-noCnstrParams proof

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

#49 - Fix warnings and get a cleaner compilation output

Pull Request - State: closed - Opened by mattam82 over 2 years ago

#48 - CertiCoq Pipeline plugin

Pull Request - State: closed - Opened by mattam82 over 2 years ago - 3 comments

#47 - Glue working with type aliases definitions

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

#46 - Direct extraction from lambda box to L2k

Pull Request - State: closed - Opened by yforster over 2 years ago - 8 comments

#45 - Fix some deprecations, update to latest metacoq version

Pull Request - State: closed - Opened by mattam82 over 2 years ago

#44 - Fix L3 -> L4 proof

Pull Request - State: closed - Opened by mattam82 almost 3 years ago

#43 - Remove equations submodule

Pull Request - State: closed - Opened by mattam82 almost 3 years ago

#42 - Update metacoq submodule

Pull Request - State: closed - Opened by mattam82 almost 3 years ago - 1 comment

#41 - Follow-up from PR #39

Pull Request - State: closed - Opened by intoverflow almost 3 years ago - 1 comment

#40 - Add benchmarks to continuous integration

Issue - State: closed - Opened by intoverflow almost 3 years ago
Labels: help wanted, good first issue

#39 - Update to Coq 8.14

Pull Request - State: closed - Opened by mattam82 almost 3 years ago - 10 comments

#38 - Compilation Issue in common/AstCommon.v and Prototype.v

Issue - State: closed - Opened by felipelisboa-ml about 3 years ago - 2 comments

#37 - Extract Constants [ ... ] fails if list contains unused constants

Issue - State: closed - Opened by intoverflow about 3 years ago - 2 comments

#36 - Compatibility with latest MetaCoq version and opam file for master (Coq 8.13)

Pull Request - State: closed - Opened by yforster over 3 years ago - 8 comments

#35 - Compatibility with latest MetaCoq version and `opam` file for `master` (Coq 8.12)

Pull Request - State: closed - Opened by yforster over 3 years ago - 1 comment

#34 - opam file

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

#33 - Added support for calling C primitive functions with tinfo

Pull Request - State: closed - Opened by zoep almost 4 years ago - 1 comment

#32 - Install OCaml also on cache hits

Pull Request - State: closed - Opened by yforster almost 4 years ago

#31 - Proper hashing of submodules for CI cache

Pull Request - State: closed - Opened by yforster almost 4 years ago - 2 comments

#30 - GitHub actions CI

Pull Request - State: closed - Opened by yforster almost 4 years ago - 2 comments

#29 - Add dearging pass on lambda box

Pull Request - State: closed - Opened by jakobbotsch almost 4 years ago - 8 comments

#28 - New glue vernacular command

Pull Request - State: closed - Opened by joom almost 4 years ago - 1 comment

#27 - Installation instructions are outdated

Issue - State: closed - Opened by spitters almost 4 years ago - 2 comments

#26 - Port master to 8.12

Pull Request - State: closed - Opened by yforster almost 4 years ago - 3 comments

#25 - Codebase cleanup

Pull Request - State: closed - Opened by zoep almost 4 years ago

#24 - Support for efficient primitives

Issue - State: open - Opened by annenkov about 4 years ago - 13 comments

#23 - Fixed a bug in erasure of primitive projection types in metacoq (no e…

Pull Request - State: closed - Opened by mattam82 about 4 years ago - 1 comment

#23 - Fixed a bug in erasure of primitive projection types in metacoq (no e…

Pull Request - State: closed - Opened by mattam82 about 4 years ago - 1 comment

#22 - Cc corresp

Pull Request - State: closed - Opened by john-ml about 4 years ago - 1 comment

#21 - Rewriter metacoq

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

#20 - Port to Coq 8.12

Pull Request - State: closed - Opened by yforster over 4 years ago - 8 comments

#19 - Make comp_data : Set

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

#18 - Update metacoq

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

#17 - Lambda lifting

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

#16 - Certicoq 8.11

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

#15 - Certicoq on 8.11

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

#14 - Certicoq on 8.10

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

#13 - Added support for function calls with parameters in glue.v + test files

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

#12 - Make install and sudo make install

Issue - State: closed - Opened by KatStark almost 5 years ago - 2 comments

#12 - Make install and sudo make install

Issue - State: closed - Opened by KatStark almost 5 years ago - 2 comments

#11 - Certicoq on Metacoq, Coq 8.9, all recent changes from master

Pull Request - State: closed - Opened by yforster about 5 years ago - 3 comments

#10 - L6 ANF from L6 CPS

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

#9 - Port to 8.9, set all submodules to 8.9 versions

Pull Request - State: closed - Opened by yforster about 5 years ago - 7 comments

#8 - Certicoq on MetaCoq

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

#7 - Compcert3.5

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

#6 - Compilation issue

Issue - State: closed - Opened by erikmd over 5 years ago - 3 comments

#5 - Move to Coq 8.8

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

#4 - compiles with the latest 8.8 branch of paramcoq

Pull Request - State: closed - Opened by aa755 over 6 years ago - 3 comments