« Up

bedrock2-compiler 0.0.2 31 m 0 s 🏆

Context

# Packages matching: installed
# Name                   # Installed # Synopsis
base-bigarray            base
base-threads             base
base-unix                base
conf-findutils           1           Virtual package relying on findutils
conf-gmp                 4           Virtual package relying on a GMP lib system installation
coq                      8.15.0      Formal proof management system
dune                     3.4.1       Fast, portable, and opinionated build system
ocaml                    4.07.1      The OCaml compiler (virtual package)
ocaml-base-compiler      4.07.1      Official release 4.07.1
ocaml-config             1           OCaml Switch Configuration
ocaml-secondary-compiler 4.08.1-1    OCaml 4.08.1 Secondary Switch Compiler
ocamlfind                1.9.1       A library manager for OCaml
ocamlfind-secondary      1.9.1       Adds support for ocaml-secondary-compiler to ocamlfind
zarith                   1.12        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.2"}
  "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.
The source language is a C-like language called ExprImp. It is an
imperative language with expressions. Currently, the only data type
is word (32-bit or 64-bit), and the memory is a partial map from words
to bytes. Records are supported as a notation for memory access with an offset.
"""
tags: ["logpath:bedrock2"]
url {
  src: "https://github.com/mit-plv/bedrock2/archive/refs/tags/v0.0.2.tar.gz"
  checksum: "sha512=4f2b2975eb3ed26158b4cf2eb6f8b2eb27fc381e57da5b0be4eb275c3306d71542938cdf614108975bf24d985b6991b95cb1f681406b9f0759f214d4eb33b337"
}

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.2 coq.8.15.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; ulimit -Sv 4000000; timeout 4h opam install -y --deps-only coq-bedrock2-compiler.0.0.2 coq.8.15.0
Return code
0
Duration
57 m 0 s

Install 🚀

Command
opam list; echo; ulimit -Sv 16000000; timeout 4h opam install -y -v coq-bedrock2-compiler.0.0.2 coq.8.15.0
Return code
0
Duration
31 m 0 s

Installation size

Total: 16 M

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

Uninstall 🧹

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

Sources are on GitHub © Guillaume Claret 🐣