« Up

riscv 0.0.3 14 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.16.1      Formal proof management system
dune                  3.12.1      Fast, portable, and opinionated build system
ocaml                 4.13.1      The OCaml compiler (virtual package)
ocaml-base-compiler   4.13.1      Official release 4.13.1
ocaml-config          2           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"
]
maintainer: "Jason Gross <jgross@mit.edu>"
homepage: "https://github.com/mit-plv/riscv-coq"
bug-reports: "https://github.com/mit-plv/riscv-coq/issues"
license: "BSD-3-Clause"
build: [
  [make "-j%{jobs}%" "EXTERNAL_DEPENDENCIES=1" "all"]
]
install: [make "EXTERNAL_DEPENDENCIES=1" "install"]
depends: [
  "coq" {>= "8.15~"}
  "coq-coqutil" {= "0.0.2"}
  "coq-record-update" {>= "0.3.0"}
]
dev-repo: "git+https://github.com/mit-plv/riscv-coq.git"
synopsis: "RISC-V Specification in Coq, somewhat experimental"
tags: ["logpath:riscv"]
url {
  src: "https://github.com/mit-plv/riscv-coq/archive/refs/tags/v0.0.3.tar.gz"
  checksum: "sha512=55c6a2aa84c89b5b4224729ccad23504d906d174d8bab9b5e1ff62dd7e76efef4935978c3ba517870d25700a1e563e2b352bb3fba94936807561840f26af75e8"
}

Lint

Command
true
Return code
0

Dry install 🏜️

Dry install with the current Coq version:

Command
opam install -y --show-action coq-riscv.0.0.3 coq.8.16.1
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-riscv.0.0.3 coq.8.16.1
Return code
0
Duration
1 m 0 s

Install 🚀

Command
opam list; echo; ulimit -Sv 16000000; timeout 4h opam install -y -v coq-riscv.0.0.3 coq.8.16.1
Return code
0
Duration
14 m 0 s

Installation size

Total: 19 M

  • 3 M ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Proofs/DecodeEncodeI.vo
  • 2 M ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Proofs/DecodeByExtension.vo
  • 1 M ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Proofs/DecodeEncodeCSR.vo
  • 863 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Proofs/DecodeEncodeI64.vo
  • 848 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Proofs/EncodeDecode.vo
  • 672 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Spec/CSRFile.vo
  • 618 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Proofs/VerifyDecode.vo
  • 517 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Proofs/DecodeEncodeM.vo
  • 326 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Proofs/DecodeEncodeA.vo
  • 321 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Utility/bverify.vo
  • 313 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Proofs/DecodeEncodeM64.vo
  • 288 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Proofs/DecodeEncodeA64.vo
  • 263 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Utility/Monads.vo
  • 260 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Examples/WMMFree.vo
  • 258 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Proofs/EncodeBound.vo
  • 221 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Platform/MinimalMMIO.vo
  • 182 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Platform/MinimalNoMul.vo
  • 180 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Platform/Minimal.vo
  • 170 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Spec/Decode.glob
  • 167 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Spec/Decode.vo
  • 157 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Utility/bverify.glob
  • 140 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Proofs/invert_encode_SB.vo
  • 132 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Platform/MetricSane.vo
  • 121 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Spec/Primitives.vo
  • 118 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Examples/WMMFree.glob
  • 117 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Proofs/invert_encode_I_shift_66.vo
  • 110 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Platform/MetricMinimalMMIO.vo
  • 108 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Spec/MetricPrimitives.vo
  • 106 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Proofs/invert_encode_UJ.vo
  • 105 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Examples/MulTrapHandler.vo
  • 100 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Platform/MinimalMMIO.glob
  • 96 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Utility/Encode.glob
  • 90 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Utility/Monads.glob
  • 89 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Platform/MetricMinimalNoMul.vo
  • 86 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Proofs/invert_encode_S.vo
  • 85 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Proofs/invert_encode_Fence.vo
  • 85 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Proofs/invert_encode_R_atomic.vo
  • 82 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Proofs/InstructionSetOrder.vo
  • 82 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Utility/Encode.vo
  • 73 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Spec/CSRGetSet.vo
  • 71 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Proofs/invert_encode_I_shift_57.vo
  • 71 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Proofs/invert_encode_R.vo
  • 71 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Platform/MinimalNoMul.glob
  • 69 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Platform/MinimalCSRs.vo
  • 68 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Proofs/invert_encode_FenceI.vo
  • 68 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Proofs/invert_encode_I.vo
  • 65 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Utility/MonadTests.vo
  • 64 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Spec/Decode.v
  • 62 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Proofs/DecodeByExtension.glob
  • 61 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Utility/InstructionNotations.vo
  • 60 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Proofs/invert_encode_I_system.vo
  • 57 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Platform/Minimal.glob
  • 57 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Spec/Machine.vo
  • 56 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Examples/SMTVerif.vo
  • 53 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Platform/MinimalMMIO_Post.vo
  • 52 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Spec/ExecuteI.vo
  • 51 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Spec/CSRGetSet.glob
  • 51 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Platform/MinimalCSRsDet.vo
  • 51 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Proofs/invert_encode_U.vo
  • 51 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Utility/RecordSettersUsingExistingGetters.vo
  • 51 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Utility/Utility.vo
  • 51 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Utility/MonadTests.glob
  • 50 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Utility/RecordSetters.vo
  • 50 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Proofs/DecodeEncodeProver.vo
  • 50 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Platform/RiscvMachine.vo
  • 48 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Platform/Memory.vo
  • 47 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Platform/AtomicMinimal.vo
  • 47 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Utility/MonadT.glob
  • 46 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Platform/MetricMinimal.vo
  • 46 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Spec/CSR.vo
  • 44 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Utility/MonadT.vo
  • 44 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Examples/WMMFree.v
  • 43 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Platform/Sane.vo
  • 43 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Examples/Fib.vo
  • 41 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Spec/CSRGetSet.v
  • 40 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Utility/FreeMonad.vo
  • 40 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Spec/ExecuteCSR.vo
  • 40 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Platform/MinimalLogging.vo
  • 38 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Platform/LogInstructionTrace.vo
  • 38 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Utility/RecordSettersUsingExistingGetters.glob
  • 38 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Spec/ExecuteA.vo
  • 38 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Spec/ExecuteA64.vo
  • 37 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Utility/JMonad.vo
  • 36 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Platform/MetricMinimalMMIO.glob
  • 35 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Platform/MaterializeRiscvProgram.vo
  • 35 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Examples/Example64Literal.vo
  • 35 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Spec/CSRField.vo
  • 34 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Spec/Primitives.glob
  • 34 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Utility/RecordSetters.glob
  • 34 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Platform/MetricRiscvMachine.vo
  • 34 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Platform/MinimalMMIO_Post.glob
  • 33 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Platform/AtomicRiscvMachine.vo
  • 33 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Proofs/EncodeDecode.glob
  • 32 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Utility/StringRecords.vo
  • 32 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Proofs/VerifyDecode.glob
  • 31 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Spec/MetricPrimitives.glob
  • 31 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Spec/ExecuteI64.vo
  • 31 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Utility/FreeMonad.glob
  • 31 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Platform/MetricLogging.vo
  • 30 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Examples/SMTVerif.glob
  • 29 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Platform/FE310ExtSpec.vo
  • 29 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Spec/ExecuteM.vo
  • 29 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Spec/PseudoInstructions.vo
  • 29 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Spec/ExecuteI.glob
  • 29 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Examples/SoftmulInsts.vo
  • 28 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Utility/JMonad.glob
  • 28 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Utility/MkMachineWidth.vo
  • 27 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Spec/ExecuteM64.vo
  • 27 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Platform/MinimalCSRs.glob
  • 26 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Platform/Run.vo
  • 26 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Platform/RiscvMachine.glob
  • 25 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Spec/Execute.vo
  • 25 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Proofs/DecodeEncode.vo
  • 24 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Utility/DefaultMemImpl64.vo
  • 24 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Utility/DefaultMemImpl32.vo
  • 24 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Utility/RegisterNames.vo
  • 24 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Utility/RecordSettersUsingExistingGetters.v
  • 24 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Utility/ExtensibleRecords.vo
  • 24 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Spec/CSRSpec.vo
  • 23 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Utility/Encode.v
  • 23 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Utility/RecordSetters.v
  • 22 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Utility/nat_div_mod_to_quot_rem.vo
  • 22 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Proofs/InstructionSetOrder.glob
  • 21 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Utility/InstructionCoercions.vo
  • 21 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Utility/StringRecords.glob
  • 21 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Platform/MetricMinimalNoMul.glob
  • 21 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Spec/VirtualMemory.vo
  • 21 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Utility/Words64Naive.vo
  • 21 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Utility/Words32Naive.vo
  • 21 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Platform/MinimalCSRsDet.glob
  • 20 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Platform/Memory.glob
  • 19 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Utility/Tactics.vo
  • 19 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Platform/MetricMinimal.glob
  • 17 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Spec/ExecuteI.v
  • 16 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Spec/CSR.glob
  • 16 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Spec/ExecuteCSR.glob
  • 16 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Examples/MulTrapHandler.glob
  • 16 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Spec/Machine.glob
  • 16 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Platform/MaterializeRiscvProgram.glob
  • 16 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Spec/ExecuteA.glob
  • 16 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Spec/ExecuteA64.glob
  • 16 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Utility/Monads.v
  • 15 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Utility/MMIOTrace.vo
  • 15 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Platform/MinimalNoMul.v
  • 14 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Utility/ExtensibleRecords.glob
  • 14 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Platform/MetricLogging.glob
  • 14 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Platform/MetricSane.glob
  • 14 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Platform/MinimalMMIO.v
  • 14 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Utility/InstructionNotations.v
  • 13 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Proofs/EncodeBound.glob
  • 13 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Platform/MetricRiscvMachine.glob
  • 12 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Platform/AtomicMinimal.glob
  • 12 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Spec/ExecuteA.v
  • 11 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Platform/AtomicRiscvMachine.glob
  • 11 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Spec/PseudoInstructions.glob
  • 11 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Utility/MonadT.v
  • 11 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Spec/ExecuteA64.v
  • 11 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Spec/ExecuteCSR.v
  • 11 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Utility/Utility.glob
  • 11 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Proofs/DecodeByExtension.v
  • 10 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Examples/SoftmulInsts.glob
  • 10 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Utility/MkMachineWidth.glob
  • 10 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Proofs/EncodeDecode.v
  • 10 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Utility/InstructionNotations.glob
  • 10 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Platform/Minimal.v
  • 10 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Utility/bverify.v
  • 10 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Utility/MonadNotations.vo
  • 9 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Platform/LogInstructionTrace.glob
  • 9 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Examples/SMTVerif.v
  • 9 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Spec/Primitives.v
  • 9 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Platform/MinimalLogging.glob
  • 9 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Utility/MonadTests.v
  • 8 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Utility/JMonad.v
  • 8 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Spec/ExecuteI64.glob
  • 8 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Spec/CSRField.glob
  • 8 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Platform/Sane.glob
  • 8 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Proofs/DecodeEncodeProver.glob
  • 7 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Examples/Fib.glob
  • 7 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Spec/ExecuteM.glob
  • 7 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Spec/MetricPrimitives.v
  • 7 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Examples/Example64Literal.glob
  • 7 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Platform/MetricMinimalMMIO.v
  • 7 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Platform/MinimalMMIO_Post.v
  • 7 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Utility/runsToNonDet.vo
  • 7 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Platform/RiscvMachine.v
  • 7 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Platform/MetricMinimal.v
  • 7 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Spec/CSRFile.glob
  • 6 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Utility/FreeMonad.v
  • 6 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Utility/runsToNonDet.glob
  • 6 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Spec/ExecuteI64.v
  • 6 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Proofs/invert_encode_I_shift_66.glob
  • 6 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Platform/MetricMinimalNoMul.v
  • 6 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Spec/ExecuteM64.glob
  • 6 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Proofs/InstructionSetOrder.v
  • 5 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Platform/MinimalCSRs.v
  • 5 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Platform/MetricSane.v
  • 5 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Spec/CSR.v
  • 5 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Utility/record_set_why_anonymous_getters.vo
  • 5 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Proofs/DecodeEncodeProver.v
  • 5 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Utility/PowerFunc.vo
  • 5 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Platform/Memory.v
  • 5 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Spec/Machine.v
  • 5 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Utility/record_set_why_anonymous_getters.glob
  • 5 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Platform/FE310ExtSpec.glob
  • 5 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Spec/ExecuteM.v
  • 4 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Utility/StringRecords.v
  • 4 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Proofs/VerifyDecode.v
  • 4 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Examples/MulTrapHandler.v
  • 4 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Platform/MetricRiscvMachine.v
  • 4 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Proofs/EncodeBound.v
  • 4 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Utility/PowerFunc.glob
  • 4 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Platform/MinimalCSRsDet.v
  • 4 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Utility/ExtensibleRecords.v
  • 4 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Platform/MetricLogging.v
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Spec/ExecuteM64.v
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Proofs/invert_encode_R_atomic.glob
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Proofs/invert_encode_Fence.glob
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Platform/MaterializeRiscvProgram.v
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Proofs/invert_encode_SB.glob
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Utility/Utility.v
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Proofs/invert_encode_I_shift_57.glob
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Platform/AtomicRiscvMachine.v
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Spec/CSRField.v
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Examples/SoftmulInsts.v
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Platform/AtomicMinimal.v
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Examples/Fib.v
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Proofs/invert_encode_R.glob
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Platform/Sane.v
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Platform/MinimalLogging.v
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Proofs/invert_encode_S.glob
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Proofs/invert_encode_I_system.glob
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Proofs/invert_encode_FenceI.glob
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Utility/nat_div_mod_to_quot_rem.glob
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Proofs/invert_encode_I.glob
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Platform/LogInstructionTrace.v
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Proofs/invert_encode_UJ.glob
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Examples/Example64Literal.v
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Spec/CSRFile.v
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Spec/Execute.glob
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Spec/PseudoInstructions.v
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Utility/RegisterNames.glob
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Platform/Run.glob
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Proofs/DecodeEncode.glob
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Utility/MkMachineWidth.v
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Proofs/invert_encode_U.glob
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Utility/runsToNonDet.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Spec/CSRSpec.glob
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Utility/DefaultMemImpl64.glob
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Utility/DefaultMemImpl32.glob
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Utility/record_set_why_anonymous_getters.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Utility/RegisterNames.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Proofs/DecodeEncode.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Platform/FE310ExtSpec.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Platform/Run.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Proofs/invert_encode_I_shift_66.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Utility/nat_div_mod_to_quot_rem.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Utility/InstructionCoercions.glob
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Utility/PowerFunc.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Proofs/DecodeEncodeM64.glob
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Proofs/DecodeEncodeI64.glob
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Proofs/DecodeEncodeCSR.glob
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Proofs/DecodeEncodeA64.glob
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Proofs/DecodeEncodeM.glob
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Proofs/DecodeEncodeI.glob
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Proofs/DecodeEncodeA.glob
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Spec/Execute.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Utility/MMIOTrace.glob
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Proofs/invert_encode_SB.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Utility/Words32Naive.glob
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Utility/Words64Naive.glob
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Proofs/invert_encode_UJ.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Utility/InstructionCoercions.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Proofs/invert_encode_R_atomic.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Proofs/invert_encode_I_shift_57.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Proofs/invert_encode_Fence.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Utility/DefaultMemImpl64.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Utility/DefaultMemImpl32.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Proofs/invert_encode_S.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Proofs/invert_encode_R.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Proofs/invert_encode_I_system.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Proofs/invert_encode_FenceI.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Proofs/invert_encode_I.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Spec/CSRSpec.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Proofs/invert_encode_U.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Utility/Tactics.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Utility/Words64Naive.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Utility/Words32Naive.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Utility/MMIOTrace.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Utility/MonadNotations.glob
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Proofs/DecodeEncodeM64.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Proofs/DecodeEncodeI64.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Proofs/DecodeEncodeCSR.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Proofs/DecodeEncodeA64.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Utility/MonadNotations.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Proofs/DecodeEncodeM.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Proofs/DecodeEncodeI.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Proofs/DecodeEncodeA.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Spec/VirtualMemory.glob
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Utility/Tactics.glob
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/riscv/Spec/VirtualMemory.v

Uninstall 🧹

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

Sources are on GitHub © Guillaume Claret 🐣