Ecosyste.ms: Issues

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

GitHub / mit-plv/bedrock2 issues and pull requests

#435 - [do not merge] Metriclightbulb

Pull Request - State: open - Opened by samuelgruetter 13 days ago - 1 comment

#434 - build fails on 32-bit

Issue - State: open - Opened by JasonGross about 1 month ago

#433 - Bump deps/kami from `de880ce` to `3ab0943`

Pull Request - State: closed - Opened by dependabot[bot] 2 months ago
Labels: submodules

#432 - Adapt to https://github.com/coq/coq/pull/19530

Pull Request - State: open - Opened by proux01 2 months ago

#431 - Leakage traces

Pull Request - State: open - Opened by OwenConoly 3 months ago - 17 comments

#430 - Document Limited LiveVerif Automation Experienced In Crit-Bit

Pull Request - State: closed - Opened by vfukala 4 months ago - 1 comment

#429 - Crit-Bit Iterators and 64-bit Compatibility

Pull Request - State: closed - Opened by vfukala 4 months ago - 1 comment

#428 - Bump deps/coqutil from `c1caa08` to `0833256`

Pull Request - State: closed - Opened by dependabot[bot] 4 months ago
Labels: submodules

#427 - Schedule submodule-update CI 15min earlier

Pull Request - State: closed - Opened by andres-erbsen 4 months ago

#426 - Bump deps/coqutil from `126561c` to `c1caa08`

Pull Request - State: closed - Opened by dependabot[bot] 4 months ago
Labels: submodules

#425 - compiler metrics

Pull Request - State: closed - Opened by tckmn 5 months ago - 3 comments

#424 - Adapt to https://github.com/coq/coq/pull/19149

Pull Request - State: closed - Opened by proux01 6 months ago - 4 comments

#423 - Bump deps/coqutil from `f12ff02` to `126561c`

Pull Request - State: closed - Opened by dependabot[bot] 6 months ago
Labels: submodules

#422 - Bump deps/coqutil from `0f3b370` to `f12ff02`

Pull Request - State: closed - Opened by dependabot[bot] 6 months ago
Labels: submodules

#421 - stop updating the tested branch

Pull Request - State: closed - Opened by andres-erbsen 7 months ago - 1 comment

#420 - Bump deps/coqutil from `a392b79` to `92bae53`

Pull Request - State: closed - Opened by dependabot[bot] 7 months ago
Labels: submodules

#419 - Schedule dependabot leading Rupicola

Pull Request - State: closed - Opened by andres-erbsen 7 months ago

#418 - [CI] Move update-tested into coq.yml

Pull Request - State: closed - Opened by JasonGross 8 months ago - 3 comments

#417 - [CI] create dependabot-automerge.yml

Pull Request - State: closed - Opened by JasonGross 8 months ago

#416 - [CI] Add coq-check-all job for ease of branch protection

Pull Request - State: closed - Opened by JasonGross 8 months ago

#415 - Adapt to https://github.com/coq/coq/pull/18880

Pull Request - State: closed - Opened by proux01 8 months ago - 4 comments

#414 - Adapt w.r.t. coq/coq#18895.

Pull Request - State: closed - Opened by ppedrot 8 months ago

#413 - Adapt w.r.t. coq/coq#18909.

Pull Request - State: closed - Opened by ppedrot 8 months ago

#412 - only_mmio_satisfying

Pull Request - State: closed - Opened by andres-erbsen 8 months ago - 1 comment

#411 - paperify lan9250_writepacket

Pull Request - State: closed - Opened by andres-erbsen 8 months ago

#410 - Bump deps/coqutil from `886fb67` to `de47a67`

Pull Request - State: closed - Opened by dependabot[bot] 8 months ago
Labels: submodules

#409 - Bump deps/coqutil from `886fb67` to `88b1403`

Pull Request - State: closed - Opened by dependabot[bot] 8 months ago - 2 comments
Labels: submodules

#408 - coqutil: coinductive version of always

Pull Request - State: closed - Opened by andres-erbsen 8 months ago

#405 - Bump deps/coqutil from `9bb864c` to `7ff6110`

Pull Request - State: closed - Opened by dependabot[bot] 9 months ago - 1 comment
Labels: submodules

#404 - adapt to coq/coq#18730

Pull Request - State: closed - Opened by andres-erbsen 9 months ago

#403 - Bump deps/coqutil from `29a3b05` to `856519e`

Pull Request - State: closed - Opened by dependabot[bot] 10 months ago
Labels: submodules

#402 - Adapt to https://github.com/coq/coq/pull/18590

Pull Request - State: closed - Opened by proux01 10 months ago - 4 comments

#401 - fully qualify coqutil.Datatypes.List.length_flat_map

Pull Request - State: closed - Opened by andres-erbsen 10 months ago

#399 - Crit-bit Trees: Lookup, Insert, Delete

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

#398 - Canceling pairs of uintptr's or uint's

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

#397 - Try assumption when checking if purified hyp already derivable

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

#396 - sepapps safe to cancel

Pull Request - State: closed - Opened by vfukala 11 months ago - 1 comment

#395 - Bump deps/coqutil from `c1f3e55` to `782f857`

Pull Request - State: closed - Opened by dependabot[bot] 11 months ago - 1 comment
Labels: submodules

#394 - Crit-bit Tree: Improve Proofs

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

#393 - dead code elimination optimization

Pull Request - State: closed - Opened by 0adb about 1 year ago - 3 comments

#392 - Bump deps/coqutil from `4b3074b` to `cd846f6`

Pull Request - State: closed - Opened by dependabot[bot] about 1 year ago - 1 comment
Labels: submodules

#391 - Don't rerun tests in bedrock2/Makefile each time

Pull Request - State: closed - Opened by samuelgruetter about 1 year ago - 2 comments

#390 - Bump deps/coq-record-update from `9928015` to `e9013a4`

Pull Request - State: closed - Opened by dependabot[bot] about 1 year ago - 1 comment
Labels: submodules

#389 - Bump deps/coqutil from `4216302` to `dae12ec`

Pull Request - State: closed - Opened by dependabot[bot] about 1 year ago - 2 comments
Labels: submodules

#388 - install target is unusable when sudo doesn't have access to coqc

Issue - State: closed - Opened by JasonGross about 1 year ago - 4 comments

#387 - Crit-bit trees

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

#386 - Use List.Forall2_nil instead of List.Forall2_refl

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

#385 - Bump deps/coqutil from `d0a5a0b` to `5b35dbb`

Pull Request - State: closed - Opened by dependabot[bot] about 1 year ago
Labels: submodules

#384 - Bump deps/coqutil from `4f2149a` to `7eb2160`

Pull Request - State: closed - Opened by dependabot[bot] about 1 year ago - 2 comments
Labels: submodules

#383 - Remove PyLevelLang from bedrock2

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

#382 - Avoid address-of-rvalue in ToCString compiler test

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

#381 - Bump deps/kami from `a5f3efe` to `c96ee95`

Pull Request - State: closed - Opened by dependabot[bot] about 1 year ago
Labels: submodules

#380 - Add export JSON and sample haskell server

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

#379 - Bump deps/coq-record-update from `9928015` to `50e45e9`

Pull Request - State: closed - Opened by dependabot[bot] about 1 year ago - 1 comment
Labels: submodules

#378 - Bump deps/coqutil from `8b84b7a` to `905ec3c`

Pull Request - State: closed - Opened by dependabot[bot] about 1 year ago - 8 comments
Labels: submodules

#375 - Bump actions/checkout from 3 to 4

Pull Request - State: closed - Opened by dependabot[bot] about 1 year ago - 2 comments
Labels: dependencies

#374 - Adapt to coq/coq#17836 (sort poly) (coqutil update)

Pull Request - State: closed - Opened by SkySkimmer about 1 year ago - 3 comments

#373 - Unbound value Int.land

Issue - State: closed - Opened by armfazh about 1 year ago - 2 comments

#372 - Fix destruct loop in straightline

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

#371 - Stop relying on `replace by` automatic `assumption`-based solving

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

#370 - design: core functionality of RecordPredicates?

Issue - State: open - Opened by andres-erbsen over 1 year ago - 4 comments

#369 - remove Stringdump in favor of PrintString

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

#368 - design: outputting bitwidth-generic code?

Issue - State: open - Opened by andres-erbsen over 1 year ago - 7 comments

#367 - Add a verified full subtractor.

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

#366 - Remove redundant notation from full_mul.v

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

#365 - Add verified Bedrock implementation of a full multiplier.

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

#364 - Wp is really exec

Pull Request - State: open - Opened by samuelgruetter over 1 year ago

#363 - Json merge

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

#362 - Wp is exec

Pull Request - State: open - Opened by andres-erbsen over 1 year ago

#361 - make `WeakestPrecondition.cmd` complete wrt `Semantics.exec`

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

#360 - Bump deps/coqutil from `b3e96d7` to `691dce4`

Pull Request - State: closed - Opened by dependabot[bot] over 1 year ago - 3 comments
Labels: submodules

#359 - Support for let bindings in fiat2->bedrock2 expression compiler

Pull Request - State: closed - Opened by psvenk over 1 year ago - 3 comments

#358 - Bump deps/coqutil from `af9cccd` to `8deac36`

Pull Request - State: closed - Opened by dependabot[bot] over 1 year ago - 1 comment
Labels: submodules

#357 - add verified polyfill adder with carry

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

#356 - Stop using auto with * in intuition

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

#355 - read Ltac2 integer bits using bitwise right shift

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

#354 - fix extraneous unfolding of get in straightline, prove addsub

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

#353 - Consolidate =* and =*>

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

#352 - Bump deps/coqutil from `f4ad731` to `5616b90`

Pull Request - State: closed - Opened by dependabot[bot] over 1 year ago - 1 comment
Labels: submodules

#351 - Bump deps/riscv-coq from `55c9cc8` to `3c623d8`

Pull Request - State: closed - Opened by dependabot[bot] over 1 year ago
Labels: submodules

#350 - Generate json eq progress

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

#349 - Expr notations and partial progress with substitute

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

#348 - [do not merge] work-in-progress dead code elimination

Pull Request - State: open - Opened by 0adb over 1 year ago

#347 - Initial progress on encoding SQL queries and related optimizations

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

#346 - Add generate json functions (Gallina and PyLevel)

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

#345 - Add IntToString unop

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

#344 - Preliminary work on expression compiler

Pull Request - State: closed - Opened by psvenk over 1 year ago - 7 comments

#343 - Bump deps/coq-record-update from `9928015` to `6c4e591`

Pull Request - State: closed - Opened by dependabot[bot] over 1 year ago - 1 comment
Labels: submodules

#342 - Reduce for lists

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

#341 - Bump deps/coq-record-update from `9928015` to `09845fe`

Pull Request - State: closed - Opened by dependabot[bot] over 1 year ago - 1 comment
Labels: submodules

#334 - Please pick the version you prefer for Coq 8.17 in Coq Platform 2023.03

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

#333 - Please pick the version you prefer for Coq 8.17 in Coq Platform 2023.03

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

#316 - Bedrock2 is broken on Coq's CI

Issue - State: closed - Opened by JasonGross almost 2 years ago - 1 comment