« Up

rupicola 0.0.4 10 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                      dev         Formal proof management system
dune                     3.1.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: [
  "Clément Pit-Claudel <clement.pitclaudel@live.com>"
  "Jade Philipoom"
  "Dustin Jamner"
  "Andres Erbsen"
  "Adam Chlipala"
]
maintainer: "Jason Gross <jgross@mit.edu>"
homepage: "https://github.com/mit-plv/rupicola"
bug-reports: "https://github.com/mit-plv/rupicola/issues"
license: "MIT"
build: [
  [make "-j%{jobs}%" "EXTERNAL_DEPENDENCIES=1" "all"]
]
install: [make "EXTERNAL_DEPENDENCIES=1" "install"]
depends: [
  "conf-findutils" {build}
  "coq" {>= "8.15~"}
  "coq-bedrock2" {= "0.0.1"}
]
dev-repo: "git+https://github.com/mit-plv/rupicola.git"
synopsis: "Gallina to imperative code compilation, currently in design phase"
tags: ["logpath:Rupicola"]
url {
  src: "https://github.com/mit-plv/rupicola/archive/refs/tags/v0.0.4.tar.gz"
  checksum: "sha512=63785a51f3495ec2df0b65977de7c9a24e08c95753da4e1852fb3b476882bda183515e948c4c6f0c8094469c3b443252c389a0c636e6addfd7db917fe0d22347"
}

Lint

Command
true
Return code
0

Dry install 🏜️

Dry install with the current Coq version:

Command
opam install -y --show-action coq-rupicola.0.0.4 coq.dev
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-rupicola.0.0.4 coq.dev
Return code
0
Duration
20 m 0 s

Install 🚀

Command
opam list; echo; ulimit -Sv 16000000; timeout 4h opam install -y -v coq-rupicola.0.0.4 coq.dev
Return code
0
Duration
10 m 0 s

Installation size

Total: 11 M

  • 528 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Lib/Core.vo
  • 423 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Lib/Loops.vo
  • 411 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/Crypto/Low.vo
  • 401 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Lib/Loops.glob
  • 401 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Lib/Core.glob
  • 392 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/Crypto/Low.glob
  • 332 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/KVStore/Manual.vo
  • 260 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Lib/Arrays.vo
  • 221 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/CapitalizeThird/Properties.vo
  • 206 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/CRC32/CRC32.vo
  • 187 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/Arrays.vo
  • 176 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/Arithmetic.vo
  • 173 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Lib/Arrays.glob
  • 172 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Lib/Compiler.vo
  • 166 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/Utf8/Utf8.vo
  • 166 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/CMove/CMove.vo
  • 163 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Lib/ExprCompiler.vo
  • 160 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/Loops.vo
  • 150 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/KVStore/Automated.vo
  • 127 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/RevComp.vo
  • 127 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/Net/IPChecksum/IPChecksum.vo
  • 121 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Lib/ControlFlow/DownTo.vo
  • 115 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Lib/NoExprReflection.vo
  • 115 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/Uppercase.vo
  • 110 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/L64X128.vo
  • 108 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Lib/ExprReflection.vo
  • 107 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/LinkedList/Find.vo
  • 104 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Lib/InlineTables.vo
  • 103 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/IO/IO.vo
  • 101 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/Cells/IndirectAdd.vo
  • 94 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/CapitalizeThird/Properties.glob
  • 92 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Lib/ExprCompiler.glob
  • 90 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/KVStore/kv.vo
  • 89 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Lib/ControlFlow/DownTo.glob
  • 88 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/IO/Echo.vo
  • 88 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Lib/ToCString.vo
  • 87 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Lib/Compiler.glob
  • 84 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/KVStore/KVStore.vo
  • 82 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Lib/Loops.v
  • 81 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Lib/Core.v
  • 81 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/Net/IPChecksum/Impl.vo
  • 78 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/Expr.vo
  • 76 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Lib/Tactics.vo
  • 74 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/Crypto/Derive.vo
  • 73 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/Nondeterminism/StackAlloc.vo
  • 70 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/LinkedList/LinkedList.vo
  • 69 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Lib/Notations.vo
  • 69 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Lib/ArrayCasts.vo
  • 67 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/Arrays.glob
  • 65 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/KVStore/Automated.glob
  • 64 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Lib/NoExprReflection.glob
  • 63 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/CMove/CMove.glob
  • 62 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/Crypto/Low.v
  • 62 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/Net/IPChecksum/Impl.glob
  • 61 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/Tree/Tree.vo
  • 61 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Lib/SepLocals.vo
  • 60 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/DownTo.vo
  • 60 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Lib/ControlFlow/CondSwap.vo
  • 60 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Lib/InlineTables.glob
  • 59 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/Nondeterminism/Peek.vo
  • 58 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/KVStore/Properties.vo
  • 58 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/IO/Stdout.vo
  • 57 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/CRC32/Table.vo
  • 57 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/Loops.glob
  • 56 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/KVStore/Tactics.vo
  • 55 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/Conditionals.vo
  • 55 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Lib/SepReflection.vo
  • 51 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/IO/Writer.vo
  • 51 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Lib/Monads.vo
  • 50 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/KVStore/kv.glob
  • 49 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/Cells/Swap.vo
  • 49 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/Nondeterminism/NonDeterminism.vo
  • 49 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/Utf8/Utils.vo
  • 48 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/Net/IPChecksum/Spec.vo
  • 47 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Lib/ExprReflection.glob
  • 47 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Lib/Alloc.vo
  • 45 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/Cells/IndirectAdd.glob
  • 45 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/IO/IO.glob
  • 45 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/Cells/Cells.vo
  • 44 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Lib/IdentParsing.vo
  • 44 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/Cells/Incr.vo
  • 43 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Lib/Conditionals.vo
  • 43 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/IO/Echo.glob
  • 42 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/Swap/Properties.vo
  • 39 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Lib/Arrays.v
  • 39 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Lib/ArrayCasts.glob
  • 39 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Lib/ToCString.glob
  • 38 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/Crypto/Spec.vo
  • 38 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Lib/Invariants.vo
  • 36 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/KVStore/Manual.glob
  • 35 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/LinkedList/Find.glob
  • 34 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Lib/ControlFlow/CondSwap.glob
  • 33 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/LinkedList/LinkedList.glob
  • 32 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/CapitalizeThird/CapitalizeThird.vo
  • 32 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/KVStore/KVStore.glob
  • 31 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Lib/WordNotations.vo
  • 31 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/Assoc/Assoc.vo
  • 31 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/Net/IPChecksum/SpecExtraction.vo
  • 30 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Lib/Notations.glob
  • 30 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/CapitalizeThird/Properties.v
  • 28 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/Arithmetic.glob
  • 28 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Lib/Api.vo
  • 27 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/Utf8/Utf8.glob
  • 27 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Lib/Compiler.v
  • 26 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/Swap/Swap.vo
  • 26 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/Expr.glob
  • 25 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Lib/ExprCompiler.v
  • 25 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/KVStore/Properties.glob
  • 25 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/Tree/Tree.glob
  • 24 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/CRC32/Table.glob
  • 24 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Lib/Conditionals.glob
  • 24 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/Nondeterminism/StackAlloc.glob
  • 22 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/IO/Stdout.glob
  • 21 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/Assoc/Assoc.glob
  • 19 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/Nondeterminism/Peek.glob
  • 18 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/IO/Writer.glob
  • 18 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/Net/IPChecksum/Spec.glob
  • 18 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Lib/ControlFlow/DownTo.v
  • 18 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/KVStore/Automated.v
  • 18 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/Nondeterminism/NonDeterminism.glob
  • 17 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Lib/Notations.v
  • 17 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/Crypto/Derive.glob
  • 17 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/Cells/Cells.glob
  • 17 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Lib/ExprReflection.v
  • 17 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Lib/SepLocals.glob
  • 16 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Lib/Gensym.vo
  • 16 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/L64X128.glob
  • 16 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Lib/SepReflection.glob
  • 16 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/Crypto/Spec.glob
  • 15 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/CRC32/CRC32.glob
  • 15 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Lib/IdentParsing.glob
  • 15 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/Conditionals.glob
  • 15 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/CapitalizeThird/CapitalizeThird.glob
  • 15 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Lib/Tactics.glob
  • 14 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Lib/Monads.glob
  • 14 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/RevComp.glob
  • 14 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Lib/NoExprReflection.v
  • 13 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Lib/Alloc.glob
  • 13 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Lib/IdentParsing.v
  • 13 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Lib/InlineTables.v
  • 13 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/Uppercase.glob
  • 13 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/KVStore/kv.v
  • 12 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Lib/Invariants.glob
  • 11 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/DownTo.glob
  • 11 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/KVStore/Tactics.glob
  • 10 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/KVStore/Manual.v
  • 10 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/Arrays.v
  • 10 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/CMove/CMove.v
  • 10 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Lib/Tactics.v
  • 10 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/Cells/Swap.glob
  • 10 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/LinkedList/Find.v
  • 10 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/Loops.v
  • 9 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/IO/IO.v
  • 9 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/Utf8/Utils.glob
  • 9 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Lib/ToCString.v
  • 9 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Lib/ArrayCasts.v
  • 9 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/Cells/Incr.glob
  • 8 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/LinkedList/LinkedList.v
  • 8 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/Net/IPChecksum/IPChecksum.glob
  • 7 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Lib/SepReflection.v
  • 7 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/KVStore/KVStore.v
  • 7 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Lib/SepLocals.v
  • 7 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/Tree/Tree.v
  • 6 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Lib/ControlFlow/CondSwap.v
  • 6 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/Net/IPChecksum/Impl.v
  • 6 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/KVStore/Tactics.v
  • 6 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Lib/Invariants.v
  • 6 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/IO/Echo.v
  • 5 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/Cells/IndirectAdd.v
  • 5 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Lib/Conditionals.v
  • 5 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Lib/Alloc.v
  • 5 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/KVStore/Properties.v
  • 4 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/Arithmetic.v
  • 4 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/Nondeterminism/StackAlloc.v
  • 4 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/Swap/Properties.glob
  • 4 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/CRC32/Table.v
  • 4 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/IO/Stdout.v
  • 4 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/IO/Writer.v
  • 4 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/Crypto/Derive.v
  • 4 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/Swap/Swap.glob
  • 4 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/RevComp.v
  • 4 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/Cells/Cells.v
  • 3 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/Nondeterminism/NonDeterminism.v
  • 3 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/CRC32/CRC32.v
  • 3 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/Nondeterminism/Peek.v
  • 3 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/Uppercase.v
  • 3 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/Expr.v
  • 3 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/Utf8/Utf8.v
  • 3 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/Net/IPChecksum/Spec.v
  • 3 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/Crypto/Spec.v
  • 3 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Lib/Monads.v
  • 3 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/Utf8/Utils.v
  • 2 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/L64X128.v
  • 2 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/Assoc/Assoc.v
  • 2 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/CapitalizeThird/CapitalizeThird.v
  • 2 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/DownTo.v
  • 2 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/Conditionals.v
  • 2 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Lib/WordNotations.glob
  • 1 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/Cells/Swap.v
  • 1 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/Net/IPChecksum/IPChecksum.v
  • 1 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Lib/WordNotations.v
  • 1 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/Swap/Properties.v
  • 1 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/Cells/Incr.v
  • 1 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Lib/Gensym.glob
  • 1 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/Net/IPChecksum/SpecExtraction.v
  • 1 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Lib/Gensym.v
  • 1 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/Swap/Swap.v
  • 1 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Lib/Api.glob
  • 1 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Lib/Api.v
  • 1 K ../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Rupicola/Examples/Net/IPChecksum/SpecExtraction.glob

Uninstall 🧹

Command
opam remove -y coq-rupicola.0.0.4
Return code
0
Missing removes
none
Wrong removes
none

Sources are on GitHub © Guillaume Claret 🐣