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

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

Pull Request - State: closed - Opened by hulsemohit almost 2 years ago

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

Pull Request - State: closed - Opened by leognon almost 2 years ago

#345 - Add IntToString unop

Pull Request - State: closed - Opened by leognon almost 2 years ago

#344 - Preliminary work on expression compiler

Pull Request - State: closed - Opened by psvenk almost 2 years ago - 7 comments

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

Pull Request - State: closed - Opened by dependabot[bot] almost 2 years ago - 1 comment
Labels: submodules

#342 - Reduce for lists

Pull Request - State: closed - Opened by hulsemohit almost 2 years ago

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

Pull Request - State: closed - Opened by dependabot[bot] almost 2 years ago - 1 comment
Labels: submodules

#340 - [in progress] working on integrating UseImmediate optimization into Pipeline.v

Pull Request - State: closed - Opened by 0adb almost 2 years ago

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

Issue - State: closed - Opened by MSoegtropIMC almost 2 years 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 almost 2 years ago - 2 comments

#316 - Bedrock2 is broken on Coq's CI

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

#100 - Allow using COQPATH to refer to bedrock2 stuff

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

#99 - Bump submodules

Issue - State: closed - Opened by JasonGross over 5 years ago - 4 comments

#98 - [do not merge] profiling for lia in bsearch.v

Pull Request - State: open - Opened by samuelgruetter over 5 years ago - 1 comment

#97 - the build output contains a lot of noise

Issue - State: open - Opened by andres-erbsen over 5 years ago - 1 comment

#96 - replace OStateND with [free] + postcondition-style interpreter

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

#95 - Avoid relying on `Export` bugs (again)

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

#94 - Automating all side conditions of binary search example

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

#93 - Kami2 SPI device verification

Pull Request - State: open - Opened by andres-erbsen-sifive over 5 years ago

#92 - Overlay for PR #9918 - refer to the right submodule for Kami

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

#91 - Fix more `Export` bugs.

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

#90 - Avoid relying on `Export` bugs

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

#89 - Makes the BytedumpTest target build on OSX.

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

#88 - Bringup4

Pull Request - State: closed - Opened by andres-erbsen-sifive over 5 years ago

#87 - Bringup3

Pull Request - State: closed - Opened by andres-erbsen-sifive over 5 years ago

#86 - Remove spurious call to PreOmega.zify

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

#84 - Bringup1

Pull Request - State: closed - Opened by andres-erbsen-sifive over 5 years ago - 1 comment

#83 - Bringup 1/?

Pull Request - State: closed - Opened by andres-erbsen-sifive over 5 years ago

#82 - standardize mmio compiler instantiation

Issue - State: open - Opened by andres-erbsen-sifive over 5 years ago

#80 - compatibility with PR #9856

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

#79 - a "getting started" guide

Issue - State: open - Opened by andres-erbsen-sifive over 5 years ago - 1 comment

#78 - splitting the repository

Issue - State: open - Opened by andres-erbsen-sifive over 5 years ago - 8 comments

#77 - prove io behavior of main loop

Pull Request - State: closed - Opened by andres-erbsen-sifive over 5 years ago - 3 comments

#76 - Update README.md: i/o and functions are implemented

Pull Request - State: closed - Opened by andres-erbsen almost 6 years ago

#75 - KamiStep_sound should cover all low-level steps

Pull Request - State: closed - Opened by andres-erbsen almost 6 years ago - 2 comments

#74 - Fibonacci Server Demo

Pull Request - State: closed - Opened by Carotti almost 6 years ago - 3 comments

#73 - proliferation of Local in files with program logic proofs

Issue - State: open - Opened by andres-erbsen almost 6 years ago - 6 comments

#72 - prove memory safety for chacha20 implementation

Pull Request - State: open - Opened by andres-erbsen almost 6 years ago - 3 comments

#71 - prove memory safety for chacha20 implementation

Pull Request - State: closed - Opened by andres-erbsen almost 6 years ago

#70 - simplify expr metrics WIP

Pull Request - State: open - Opened by andres-erbsen almost 6 years ago

#69 - duplication of Instance definitions after removal of primitive projections

Issue - State: closed - Opened by andres-erbsen almost 6 years ago - 1 comment

#68 - Add metrics to compilation process

Pull Request - State: closed - Opened by Carotti almost 6 years ago - 13 comments

#67 - add support in the program logic for 16/32-bit loads/stores

Pull Request - State: closed - Opened by jmgrosen almost 6 years ago - 1 comment

#66 - Thesis

Pull Request - State: closed - Opened by cl-wood almost 6 years ago - 1 comment

#65 - Checking for anomalies

Pull Request - State: closed - Opened by cl-wood almost 6 years ago

#64 - Factor out bitwidth-specific part of large literals proof

Pull Request - State: closed - Opened by tchajed almost 6 years ago

#63 - feature request: linking readonly data

Issue - State: open - Opened by andres-erbsen almost 6 years ago - 4 comments

#62 - ecancel_assumption triggers unification

Issue - State: closed - Opened by samuelgruetter almost 6 years ago - 2 comments

#61 - consolidate bedrock2.Syntax.Basic; port examples

Pull Request - State: closed - Opened by andres-erbsen almost 6 years ago - 1 comment

#60 - kami needs bbv, add bbv submodule?

Issue - State: closed - Opened by andres-erbsen almost 6 years ago - 4 comments

#59 - consider git.sr.ht + builds.sr.ht instead of github+travis

Issue - State: open - Opened by andres-erbsen almost 6 years ago - 4 comments

#58 - Please bump submodules

Issue - State: closed - Opened by JasonGross about 6 years ago - 2 comments

#57 - Fix build on Windows

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

#56 - feature request: make clean (that'd be safer than git clean -dxf)

Issue - State: closed - Opened by andres-erbsen about 6 years ago - 2 comments

#55 - feature request: make up to specific .vo

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

#54 - Only allow one open goal at a time

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

#53 - feature request: hex constants

Issue - State: closed - Opened by andres-erbsen about 6 years ago - 9 comments

#52 - program logic proofs are slow in PG, patch it

Issue - State: open - Opened by andres-erbsen about 6 years ago

#51 - [do not merge yet] Connect to Kami

Pull Request - State: closed - Opened by samuelgruetter about 6 years ago - 3 comments

#50 - sketch squarer program with IO

Pull Request - State: closed - Opened by samuelgruetter about 6 years ago - 2 comments

#49 - Why was the decision made to not support function pointers?

Issue - State: closed - Opened by jeremysalwen about 6 years ago - 2 comments

#48 - test 8.9beta in travis

Issue - State: closed - Opened by andres-erbsen about 6 years ago - 3 comments

#47 - Update README.md

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

#46 - bedrock2.Semantics: commit to two's complement

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

#45 - all files should Global Unset Refine Instance Mode

Issue - State: closed - Opened by andres-erbsen about 6 years ago - 3 comments

#44 - Optimization: Boolean expression compiler

Pull Request - State: closed - Opened by stellamplau about 6 years ago - 2 comments

#43 - word library specification

Issue - State: closed - Opened by andres-erbsen about 6 years ago - 9 comments

#42 - remove wsplit, make word non-indexed

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

#41 - allow weakening of locals map in program logic

Issue - State: open - Opened by andres-erbsen about 6 years ago

#40 - variable scoping and program logic

Issue - State: closed - Opened by andres-erbsen about 6 years ago - 2 comments

#39 - liveness analysis draft

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

#38 - seq associativity

Issue - State: closed - Opened by andres-erbsen about 6 years ago

#37 - warnings policy?

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

#36 - implement cmd.unset for declaring a variable dead

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

#35 - liveness analysis

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

#34 - tweak locals notation

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

#33 - consolidate and factor out map library

Issue - State: closed - Opened by andres-erbsen about 6 years ago - 5 comments

#32 - Boolean equality on bytes is incorrect

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

#31 - Comply with coq#8745

Pull Request - State: closed - Opened by andres-erbsen over 6 years ago

#30 - Proposal: Globals (pre-cursor to Compilation Units)

Pull Request - State: open - Opened by gmalecha over 6 years ago - 5 comments

#29 - Bedrock2 notation breaks record notation

Issue - State: closed - Opened by gmalecha over 6 years ago - 4 comments

#28 - Split Machine-specific and language-specific parameters

Issue - State: open - Opened by gmalecha over 6 years ago - 3 comments

#27 - Define a semantics in the bedrock2 directory

Issue - State: closed - Opened by gmalecha over 6 years ago - 3 comments

#26 - Arrays and structs

Pull Request - State: closed - Opened by gmalecha over 6 years ago - 5 comments

#25 - [do not merge] try to move bedrock2.BasicC64Syntax.BasicALU to a more generic place

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

#24 - Import prim token notations before using them

Pull Request - State: closed - Opened by JasonGross over 6 years ago - 5 comments

#23 - bedrock2 is incompatible with numeral notations

Issue - State: closed - Opened by JasonGross over 6 years ago - 2 comments

#22 - don't change Syntax.parameters when StringNames is imported

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

#21 - separate names for the various parameter typeclasses

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

#20 - link to public version of bbv library

Pull Request - State: closed - Opened by maxsnew over 6 years ago - 1 comment

#19 - bedrock2.Syntax.parameters needs a better name

Issue - State: closed - Opened by samuelgruetter over 6 years ago - 3 comments

#18 - ensure and test that return values are assigned left to right

Issue - State: closed - Opened by andres-erbsen over 6 years ago - 3 comments

#17 - feature requests from kernel programmers

Issue - State: open - Opened by andres-erbsen over 6 years ago - 7 comments

#16 - [do not merge, but fork] Refactoring

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

#15 - [do not merge] starting register allocation and sets/maps refactoring

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

#14 - [do not merge] semantics-refactor

Pull Request - State: open - Opened by samuelgruetter over 6 years ago - 3 comments

#13 - state_calc should fail if it doesnt find key_eq_dec

Issue - State: open - Opened by andres-erbsen over 6 years ago - 1 comment