mit-plv/bedrock2

Issues

• [coq-bedrock2] Please create a tag for Coq 8.19 in Coq Platform 2024.01

  #406 opened 9 months ago by rtetley
  0

• [coq-bedrock2-compiler] Please create a tag for Coq 8.19 in Coq Platform 2024.01

  #407 opened 9 months ago by rtetley
  0

• install target is unusable when sudo doesn't have access to coqc

  #388 opened a year ago by JasonGross
  4

• Please pick the version you prefer for Coq 8.18 in Coq Platform 2023.10 [coq-bedrock2-compiler]

  #377 opened a year ago by rtetley
  2

• Please pick the version you prefer for Coq 8.18 in Coq Platform 2023.10 [coq-bedrock2]

  #376 opened a year ago by rtetley
  2

• Unbound value Int.land

  #373 opened a year ago by armfazh
  2

• design: core functionality of RecordPredicates?

  #370 opened a year ago by andres-erbsen
  4

• design: outputting bitwidth-generic code?

  #368 opened a year ago by andres-erbsen
  7

• Bedrock2 is broken on Coq's CI

  #316 opened 2 years ago by JasonGross
  1

• Please pick the version you prefer for Coq 8.17 in Coq Platform 2023.03

  #334 opened 2 years ago by MSoegtropIMC
  2

• Please pick the version you prefer for Coq 8.17 in Coq Platform 2023.03

  #333 opened 2 years ago by MSoegtropIMC
  2

• Update tested is failing with rate limits

  #309 opened 2 years ago by JasonGross
  2

• `make` should not run `coq` and `cc` when there's nothing to be done

  #298 opened 2 years ago by JasonGross
  0

• ecancel_assumption failure

  #174 opened 2 years ago by RasmusHoldsbjergCSAU
  3

• how to avoid breakage with coq master?

  #121 opened 2 years ago by andres-erbsen
  13

• Bytedump.v fails to build on Windows

  #146 opened 2 years ago by JasonGross
  3

• Failing in coq CI

  #288 opened 2 years ago by SkySkimmer
  1

• Less Memory-Hungry, More Principled Solution for Decidable Side-Conditions

  #285 opened 2 years ago by JasonGross
  2

• bedrock2 lightbulb example is incompatible with native_compute

  #282 opened 2 years ago by JasonGross
  5

• Please create a tag for Coq 8.16 in Coq Platform 2022.09

  #268 opened 2 years ago by MSoegtropIMC
  6

• bedrock2 fails with a syntax error on Windows

  #273 opened 2 years ago by JasonGross
  9

• Why does bedrock2 use `Load`?

  #224 opened 3 years ago by JasonGross
  2

• Using multiple return values

  #222 opened 3 years ago by RasmusHoldsbjergCSAU
  2

• stackloop: `main` should return `int`, not `void`

  #220 opened 3 years ago by samuelgruetter
  1

• bedrock2.NotationsCustomEntry breaks Tactic Notation

  #165 opened 3 years ago by samuelgruetter
  6

• Move MMIO.v

  #205 opened 3 years ago by JasonGross
  3

• Test suite for ToCString

  #204 opened 3 years ago by andres-erbsen
  1

• predicates describing bytes in memory

  #185 opened 4 years ago by andres-erbsen
  3

• bedrock1 CPS semantics vs bedrock2 postcondition semantics

  #198 opened 3 years ago by spitters
  1

• Hint Mode + again

  #193 opened 3 years ago by samuelgruetter
  9

• Makefile doesn't work with EXTERNAL_DEPENDENCIES=1

  #192 opened 3 years ago by Alizter
  4

• Missing operators

  #189 opened 4 years ago by samuelgruetter
  1

• Best practice for proving loop termination in firmware?

  #186 opened 4 years ago by jadephilipoom
  22

• Platform

  #176 opened 4 years ago by spitters
  4

• Missing variable declaration in printed C function when using stack allocation.

  #175 opened 4 years ago by RasmusHoldsbjergCSAU
  2

• opam package for bench

  #170 opened 4 years ago by SkySkimmer
  1

• [request] c_call like c_func / fmt_c_decl

  #168 opened 4 years ago by JasonGross
  2

• straightline_cleanup turns provable goal unprovable

  #167 opened 4 years ago by bdiehs
  4

• standards conformance of the C backend

  #160 opened 4 years ago by andres-erbsen
  2

• load8 vs load_word?

  #159 opened 4 years ago by andres-erbsen
  5

• incorporate bytes<->words conversion from fiat-crypto

  #156 opened 5 years ago by andres-erbsen
  6

• Semantics.parameters_ok instance for BasicC32Semantics

  #151 opened 5 years ago by jadephilipoom
  1

• Does bedrock2 want warning/error annotations on PRs?

  #149 opened 5 years ago by JasonGross
  4

• CI failure

  #148 opened 5 years ago by JasonGross
  1

• Multiplication is missing

  #139 opened 5 years ago by jadephilipoom
  4

• WeakestPreconditionProperties takes more than 5x as much RAM as anything else in bedrock2_noex

  #130 opened 5 years ago by JasonGross
  0

• Travis spuriously uses Coq 8.4 instead of master

  #123 opened 5 years ago by samuelgruetter
  2

• bedrock2 tip does not build on Coq master

  #120 opened 5 years ago by JasonGross
  6

• bedrock2 fails to build when switching from EXTERNAL_DEPENDENCIES=1 to EXTERNAL_DEPENDENCIES= because _CoqProject is not remade

  #119 opened 5 years ago by JasonGross
  2

• make -k does not build compiler if bedrock2 fails

  #114 opened 5 years ago by andres-erbsen
  1