« Up

rupicola 0.0.5 4 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.1      Formal proof management system
dune                  3.6.2       Fast, portable, and opinionated build system
ocaml                 4.14.0      The OCaml compiler (virtual package)
ocaml-base-compiler   4.14.0      Official release 4.14.0
ocaml-config          2           OCaml Switch Configuration
ocaml-options-vanilla 1           Ensure that OCaml is compiled with no special options enabled
ocamlfind             1.9.5       A library manager for OCaml
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.2" & <= "0.0.4"}
]
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.5.tar.gz"
  checksum: "sha512=708c58be12b8756815343a20026d5c277b1e5d84ae2903eb4e234558891f4f4d7d3c814971f4bf2916e05bc448be897fc249d32e5c84ef7d405f5456b1efdd6d"
}

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.5 coq.8.15.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-rupicola.0.0.5 coq.8.15.1
Return code
0
Duration
18 m 0 s

Install 🚀

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

Installation size

Total: 10 M

  • 414 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Lib/Loops.vo
  • 401 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Lib/Loops.glob
  • 330 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Examples/KVStore/Manual.vo
  • 314 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Lib/Core.vo
  • 252 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Lib/Arrays.vo
  • 228 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Lib/Core.glob
  • 216 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Examples/CapitalizeThird/Properties.vo
  • 206 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Examples/CRC32/CRC32.vo
  • 184 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Examples/Arrays.vo
  • 177 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Examples/Arithmetic.vo
  • 173 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Lib/Arrays.glob
  • 171 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Lib/Compiler.vo
  • 167 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Examples/Utf8/Utf8.vo
  • 165 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Examples/CMove/CMove.vo
  • 160 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Examples/Loops.vo
  • 148 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Examples/KVStore/Automated.vo
  • 146 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Lib/ExprCompiler.vo
  • 129 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Examples/Net/IPChecksum/IPChecksum.vo
  • 128 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Examples/RevComp.vo
  • 121 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Lib/ControlFlow/DownTo.vo
  • 115 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Examples/Uppercase.vo
  • 114 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Lib/NoExprReflection.vo
  • 111 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Examples/L64X128.vo
  • 108 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Lib/ExprReflection.vo
  • 107 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Examples/LinkedList/Find.vo
  • 103 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Examples/IO/IO.vo
  • 103 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Lib/InlineTables.vo
  • 101 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Examples/Cells/IndirectAdd.vo
  • 93 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Examples/CapitalizeThird/Properties.glob
  • 92 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Examples/KVStore/kv.vo
  • 92 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Lib/ExprCompiler.glob
  • 89 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Lib/ControlFlow/DownTo.glob
  • 88 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Lib/ToCString.vo
  • 87 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Examples/IO/Echo.vo
  • 87 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Lib/Compiler.glob
  • 85 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Examples/KVStore/KVStore.vo
  • 83 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Examples/Net/IPChecksum/Impl.vo
  • 82 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Lib/Loops.v
  • 78 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Examples/Expr.vo
  • 77 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Lib/Tactics.vo
  • 75 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Examples/Net/IPChecksum/Impl.glob
  • 73 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Examples/Nondeterminism/StackAlloc.vo
  • 71 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Lib/Notations.vo
  • 70 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Examples/LinkedList/LinkedList.vo
  • 67 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Examples/Arrays.glob
  • 65 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Examples/KVStore/Automated.glob
  • 64 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Lib/NoExprReflection.glob
  • 63 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Examples/CMove/CMove.glob
  • 62 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Examples/Tree/Tree.vo
  • 61 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Examples/DownTo.vo
  • 61 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Lib/ControlFlow/CondSwap.vo
  • 61 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Lib/SepLocals.vo
  • 60 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Examples/Nondeterminism/Peek.vo
  • 59 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Lib/InlineTables.glob
  • 58 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Examples/IO/Stdout.vo
  • 57 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Examples/CRC32/Table.vo
  • 57 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Examples/Loops.glob
  • 57 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Examples/KVStore/Tactics.vo
  • 56 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Examples/Conditionals.vo
  • 56 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Examples/KVStore/Properties.vo
  • 56 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Lib/SepReflection.vo
  • 52 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Examples/IO/Writer.vo
  • 52 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Lib/Monads.vo
  • 50 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Examples/Cells/Swap.vo
  • 50 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Examples/Nondeterminism/NonDeterminism.vo
  • 50 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Examples/KVStore/kv.glob
  • 49 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Examples/Utf8/Utils.vo
  • 48 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Examples/Net/IPChecksum/Spec.vo
  • 48 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Lib/Core.v
  • 48 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Lib/Alloc.vo
  • 47 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Lib/ExprReflection.glob
  • 45 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Examples/Cells/Cells.vo
  • 45 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Examples/Cells/Incr.vo
  • 45 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Examples/Cells/IndirectAdd.glob
  • 45 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Examples/IO/IO.glob
  • 45 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Lib/IdentParsing.vo
  • 44 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Lib/Conditionals.vo
  • 43 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Examples/Swap/Properties.vo
  • 43 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Examples/IO/Echo.glob
  • 39 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Lib/Arrays.v
  • 39 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Lib/ToCString.glob
  • 39 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Lib/Invariants.vo
  • 36 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Examples/KVStore/Manual.glob
  • 35 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Examples/LinkedList/Find.glob
  • 35 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Lib/ControlFlow/CondSwap.glob
  • 33 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Examples/CapitalizeThird/CapitalizeThird.vo
  • 33 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Examples/LinkedList/LinkedList.glob
  • 32 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Lib/WordNotations.vo
  • 32 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Examples/KVStore/KVStore.glob
  • 31 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Examples/Net/IPChecksum/SpecExtraction.vo
  • 31 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Examples/Assoc/Assoc.vo
  • 30 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Lib/Notations.glob
  • 30 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Examples/CapitalizeThird/Properties.v
  • 29 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Lib/Api.vo
  • 28 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Examples/Arithmetic.glob
  • 27 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Examples/Utf8/Utf8.glob
  • 27 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Lib/Compiler.v
  • 27 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Examples/Swap/Swap.vo
  • 26 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Examples/Expr.glob
  • 25 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Lib/ExprCompiler.v
  • 25 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Examples/KVStore/Properties.glob
  • 25 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Examples/Tree/Tree.glob
  • 24 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Examples/CRC32/Table.glob
  • 24 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Lib/Conditionals.glob
  • 24 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Examples/Nondeterminism/StackAlloc.glob
  • 22 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Examples/IO/Stdout.glob
  • 21 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Examples/Assoc/Assoc.glob
  • 19 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Examples/Nondeterminism/Peek.glob
  • 18 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Examples/IO/Writer.glob
  • 18 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Examples/Net/IPChecksum/Spec.glob
  • 18 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Lib/ControlFlow/DownTo.v
  • 18 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Examples/KVStore/Automated.v
  • 18 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Examples/Nondeterminism/NonDeterminism.glob
  • 17 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Lib/Notations.v
  • 17 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Examples/Cells/Cells.glob
  • 17 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Lib/ExprReflection.v
  • 17 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Lib/SepLocals.glob
  • 16 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Lib/Gensym.vo
  • 16 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Examples/L64X128.glob
  • 16 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Lib/SepReflection.glob
  • 15 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Examples/CRC32/CRC32.glob
  • 15 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Lib/IdentParsing.glob
  • 15 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Examples/Conditionals.glob
  • 15 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Examples/CapitalizeThird/CapitalizeThird.glob
  • 15 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Lib/Tactics.glob
  • 14 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Lib/Monads.glob
  • 14 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Examples/RevComp.glob
  • 14 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Lib/NoExprReflection.v
  • 13 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Lib/Alloc.glob
  • 13 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Lib/IdentParsing.v
  • 13 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Lib/InlineTables.v
  • 13 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Examples/Uppercase.glob
  • 13 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Examples/KVStore/kv.v
  • 12 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Lib/Invariants.glob
  • 11 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Examples/DownTo.glob
  • 11 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Examples/KVStore/Tactics.glob
  • 10 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Examples/KVStore/Manual.v
  • 10 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Examples/Arrays.v
  • 10 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Examples/CMove/CMove.v
  • 10 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Lib/Tactics.v
  • 10 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Examples/Cells/Swap.glob
  • 10 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Examples/LinkedList/Find.v
  • 10 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Examples/Loops.v
  • 9 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Examples/IO/IO.v
  • 9 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Examples/Utf8/Utils.glob
  • 9 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Lib/ToCString.v
  • 9 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Examples/Cells/Incr.glob
  • 8 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Examples/LinkedList/LinkedList.v
  • 8 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Examples/Net/IPChecksum/IPChecksum.glob
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Lib/SepReflection.v
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Examples/KVStore/KVStore.v
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Lib/SepLocals.v
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Examples/Tree/Tree.v
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Examples/Net/IPChecksum/Impl.v
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Lib/ControlFlow/CondSwap.v
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Examples/KVStore/Tactics.v
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Lib/Invariants.v
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Examples/IO/Echo.v
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Examples/Cells/IndirectAdd.v
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Lib/Conditionals.v
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Lib/Alloc.v
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Examples/KVStore/Properties.v
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Examples/Arithmetic.v
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Examples/Nondeterminism/StackAlloc.v
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Examples/Swap/Properties.glob
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Examples/CRC32/Table.v
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Examples/IO/Stdout.v
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Examples/IO/Writer.v
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Examples/Swap/Swap.glob
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Examples/RevComp.v
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Examples/Cells/Cells.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Examples/Nondeterminism/NonDeterminism.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Examples/CRC32/CRC32.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Examples/Nondeterminism/Peek.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Examples/Uppercase.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Examples/Expr.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Examples/Utf8/Utf8.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Examples/Net/IPChecksum/Spec.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Lib/Monads.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Examples/Utf8/Utils.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Examples/L64X128.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Examples/Assoc/Assoc.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Examples/CapitalizeThird/CapitalizeThird.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Examples/DownTo.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Examples/Conditionals.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Lib/WordNotations.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Examples/Cells/Swap.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Examples/Net/IPChecksum/IPChecksum.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Lib/WordNotations.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Examples/Swap/Properties.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Examples/Cells/Incr.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Lib/Gensym.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Examples/Net/IPChecksum/SpecExtraction.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Lib/Gensym.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Examples/Swap/Swap.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Lib/Api.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Lib/Api.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Rupicola/Examples/Net/IPChecksum/SpecExtraction.glob

Uninstall 🧹

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

Sources are on GitHub © Guillaume Claret 🐣