« Up

bedrock2-compiler 0.0.3 10 m 0 s 🏆

Context

# Packages matching: installed
# Name                # Installed # Synopsis
base-bigarray         base
base-domains          base
base-nnp              base        Naked pointers prohibited in the OCaml heap
base-threads          base
base-unix             base
conf-gmp              4           Virtual package relying on a GMP lib system installation
coq                   8.17.0      The Coq Proof Assistant
coq-core              8.17.0      The Coq Proof Assistant -- Core Binaries and Tools
coq-stdlib            8.17.0      The Coq Proof Assistant -- Standard Library
coqide-server         8.17.0      The Coq Proof Assistant, XML protocol server
dune                  3.12.2      Fast, portable, and opinionated build system
ocaml                 5.1.1       The OCaml compiler (virtual package)
ocaml-base-compiler   5.1.1       Official release 5.1.1
ocaml-config          3           OCaml Switch Configuration
ocaml-options-vanilla 1           Ensure that OCaml is compiled with no special options enabled
ocamlfind             1.9.6       A library manager for OCaml
zarith                1.13        Implements arithmetic and logical operations over arbitrary-precision integers
# opam file:
opam-version: "2.0"
authors: [
  "Massachusetts Institute of Technology"
  "Kevix"
  "SiFive"
]
maintainer: "Jason Gross <jgross@mit.edu>"
homepage: "https://github.com/mit-plv/bedrock2"
bug-reports: "https://github.com/mit-plv/bedrock2/issues"
license: "MIT"
build: [
  # No reason to build compiler_ex since there's no install_compiler_ex target; the install_compiler target installs only compiler_noex
  [make "-j%{jobs}%" "EXTERNAL_DEPENDENCIES=1" "compiler_noex"]
]
install: [make "EXTERNAL_DEPENDENCIES=1" "install_compiler"]
depends: [
  "conf-findutils" {build}
  "coq" {>= "8.15~"}
  "coq-bedrock2" {= "0.0.3"}
  "coq-riscv" {= "0.0.2"}
  "zarith" {>= "1.11"}
]
dev-repo: "git+https://github.com/mit-plv/bedrock2.git"
synopsis: "A work-in-progress language and compiler for verified low-level programming (compiler part)"
description: """
bedrock2 is a low-level systems programming language. This language is
equipped with a simple program logic for proving correctness of the
programs.  This package includes a verified compiler targeting RISC-V
from this language.
The project has similar goals as bedrock, but uses a different design.
No code is shared between bedrock and bedrock2.
"""
tags: ["logpath:bedrock2"]
url {
  src: "https://github.com/mit-plv/bedrock2/archive/refs/tags/v0.0.3.tar.gz"
  checksum: "sha512=935d6f0ca45b43f789af381ed654ef016ea28ff40acbfcac13eaf1ea297a9cd86c14e9199dd6bde28e71fae662b6b06e52999759f8467a8fbe2f1daf9a3de592"
}

Lint

Command
true
Return code
0

Dry install 🏜️

Dry install with the current Coq version:

Command
opam install -y --show-action coq-bedrock2-compiler.0.0.3 coq.8.17.0
Return code
0

Dry install without Coq/switch base, to test if the problem was incompatibility with the current Coq/OCaml version:

Command
true
Return code
0

Install dependencies

Command
opam list; echo; timeout 4h opam install -y --deps-only coq-bedrock2-compiler.0.0.3 coq.8.17.0
Return code
0
Duration
13 m 0 s

Install 🚀

Command
opam list; echo; timeout 4h opam install -y -v coq-bedrock2-compiler.0.0.3 coq.8.17.0
Return code
0
Duration
10 m 0 s

Installation size

Total: 16 M

  • 3 M ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/FlatToRiscvFunctions.vo
  • 2 M ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/FlattenExpr.vo
  • 881 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/Spilling.vo
  • 798 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/FlatToRiscvMetric.vo
  • 708 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/RegAlloc.vo
  • 612 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/SpillingMapGoals.vo
  • 450 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/MMIO.vo
  • 406 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/FlattenExpr.glob
  • 398 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/ToplevelLoop.vo
  • 386 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/FlatImp.vo
  • 312 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/LowerPipeline.vo
  • 290 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/FlatToRiscvCommon.vo
  • 282 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/RunInstruction.vo
  • 265 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/ExprImp.vo
  • 260 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/Spilling.glob
  • 241 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/FlatToRiscvLiterals.vo
  • 233 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/FlatToRiscvFunctions.glob
  • 202 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/Pipeline.vo
  • 192 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/SeparationLogic.vo
  • 185 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/RegAlloc.glob
  • 175 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/GoFlatToRiscv.vo
  • 159 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/load_save_regs_correct.vo
  • 155 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/EmitsValid.vo
  • 150 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/FlatToRiscvCommon.glob
  • 148 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/Registers.vo
  • 125 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/GoFlatToRiscv.glob
  • 122 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/FitsStack.vo
  • 119 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/FlatImp.glob
  • 108 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/CompilerInvariant.vo
  • 99 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/LowerPipeline.glob
  • 94 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/SeparationLogic.glob
  • 85 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/ExprImp.glob
  • 80 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/FlatToRiscvFunctions.v
  • 79 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/Pipeline.glob
  • 73 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/Spilling.v
  • 69 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/ToplevelLoop.glob
  • 67 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/RiscvEventLoop.vo
  • 63 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/UniqueSepLog.vo
  • 63 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/RunInstruction.glob
  • 60 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/FlatImpSepLog.vo
  • 60 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/FlatToRiscvDef.vo
  • 59 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/FlatImpUniqueSepLog.vo
  • 56 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/StringNameGen.vo
  • 54 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/FlattenExprDef.vo
  • 51 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/FlatToRiscvDef.glob
  • 50 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/util/Result.vo
  • 50 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/MMIO.glob
  • 48 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/ForeverSafe.vo
  • 46 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/ZLemmas.vo
  • 45 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/RegAlloc.v
  • 44 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/EmitsValid.glob
  • 44 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/FitsStack.glob
  • 43 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/ExprImpEventLoopSpec.vo
  • 42 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/FlatImpUniqueSepLog.glob
  • 41 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/FlatToRiscvMetric.glob
  • 40 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/FlatImpSepLog.glob
  • 39 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/FlatToRiscvCommon.v
  • 39 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/FlattenExpr.v
  • 38 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/DivisibleBy4.vo
  • 35 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/MemoryLayout.vo
  • 34 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/GoFlatToRiscv.v
  • 33 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/FlatToRiscvLiterals.glob
  • 33 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/FlattenExprDef.glob
  • 33 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/UniqueSepLog.glob
  • 33 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/CompilerInvariant.glob
  • 32 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/RiscvWordProperties.vo
  • 32 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/NaiveRiscvWordProperties.vo
  • 31 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/mod4_0.vo
  • 31 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/LowerPipeline.v
  • 29 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/ZNameGen.vo
  • 28 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/regs_initialized.vo
  • 27 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/FlatImpConstraints.vo
  • 26 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/load_save_regs_correct.glob
  • 26 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/FlatImp.v
  • 25 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/NameGen.vo
  • 25 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/Symbols.vo
  • 24 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/ToplevelLoop.v
  • 24 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/Pipeline.v
  • 23 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/SeparationLogic.v
  • 23 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/NaiveRiscvWordProperties.glob
  • 23 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/util/Common.vo
  • 22 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/ExprImp.v
  • 20 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/MetricsToRiscv.vo
  • 20 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/util/Result.glob
  • 19 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/MMIO.v
  • 16 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/RunInstruction.v
  • 16 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/StringNameGen.glob
  • 16 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/EmitsValid.v
  • 15 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/RiscvEventLoop.glob
  • 15 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/ZLemmas.glob
  • 14 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/SpillingMapGoals.glob
  • 14 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/FlatToRiscvDef.v
  • 14 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/FlatToRiscvMetric.v
  • 13 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/ForeverSafe.glob
  • 13 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/UniqueSepLog.v
  • 12 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/DivisibleBy4.glob
  • 12 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/Registers.glob
  • 10 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/mod4_0.glob
  • 9 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/CompilerInvariant.v
  • 9 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/RiscvWordProperties.glob
  • 9 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/FitsStack.v
  • 9 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/load_save_regs_correct.v
  • 8 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/FlatToRiscvLiterals.v
  • 8 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/FlattenExprDef.v
  • 8 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/ExprImpEventLoopSpec.glob
  • 7 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/FlatImpSepLog.v
  • 7 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/FlatImpUniqueSepLog.v
  • 6 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/util/Misc.vo
  • 6 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/util/Learning.vo
  • 6 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/RiscvEventLoop.v
  • 6 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/GenericForeverSafe.glob
  • 5 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/GenericForeverSafe.vo
  • 5 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/util/Result.v
  • 5 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/StringNameGen.v
  • 5 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/ForeverSafe.v
  • 5 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/regs_initialized.glob
  • 5 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/ZNameGen.glob
  • 4 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/DivisibleBy4.v
  • 4 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/Registers.v
  • 4 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/util/Misc.glob
  • 4 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/MemoryLayout.glob
  • 4 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/NaiveRiscvWordProperties.v
  • 4 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/on_hyp_containing.vo
  • 4 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/SpillingMapGoals.v
  • 4 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/Symbols.glob
  • 3 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/ZLemmas.v
  • 3 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/eqexact.vo
  • 3 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/NameGen.glob
  • 3 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/FlatImpConstraints.glob
  • 2 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/mod4_0.v
  • 2 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/util/LogGoal.vo
  • 2 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/ExprImpEventLoopSpec.v
  • 2 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/MetricsToRiscv.glob
  • 2 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/RiscvWordProperties.v
  • 2 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/regs_initialized.v
  • 2 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/GenericForeverSafe.v
  • 2 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/util/Learning.glob
  • 1 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/ZNameGen.v
  • 1 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/MemoryLayout.v
  • 1 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/util/Learning.v
  • 1 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/MetricsToRiscv.v
  • 1 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/Symbols.v
  • 1 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/NameGen.v
  • 1 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/eqexact.v
  • 1 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/on_hyp_containing.v
  • 1 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/FlatImpConstraints.v
  • 1 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/util/Misc.v
  • 1 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/util/Common.glob
  • 1 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/util/Common.v
  • 1 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/util/LogGoal.v
  • 1 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/on_hyp_containing.glob
  • 1 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/util/LogGoal.glob
  • 1 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/compiler/eqexact.glob

Uninstall 🧹

Command
opam remove -y coq-bedrock2-compiler.0.0.3
Return code
0
Missing removes
none
Wrong removes
none

Sources are on GitHub © Guillaume Claret 🐣