« Up

fairisle 8.10.0 1 m 26 s

(2020-07-14 04:23:34 UTC)

Context

# Packages matching: installed
# Name              # Installed # Synopsis
base-bigarray       base
base-num            base        Num library distributed with the OCaml compiler
base-threads        base
base-unix           base
conf-findutils      1           Virtual package relying on findutils
conf-m4             1           Virtual package relying on m4
coq                 8.10.0      Formal proof management system
num                 0           The Num library for arbitrary-precision integer and rational arithmetic
ocaml               4.05.0      The OCaml compiler (virtual package)
ocaml-base-compiler 4.05.0      Official 4.05.0 release
ocaml-config        1           OCaml Switch Configuration
ocamlfind           1.8.1       A library manager for OCaml
# opam file:
opam-version: "2.0"
maintainer: "Hugo.Herbelin@inria.fr"
homepage: "https://github.com/http://www.dil.univ-mrs.fr/~jakubiec/fairisle.tar.gz"
license: "LGPL 2.1"
build: [make "-j%{jobs}%"]
install: [make "install"]
remove: ["rm" "-R" "%{lib}%/coq/user-contrib/Fairisle"]
depends: [
  "ocaml"
  "coq" {>= "8.10" & < "8.11~"}
]
tags: [
  "keyword: circuits"
  "keyword: automata"
  "keyword: co-induction"
  "keyword: dependent types."
  "category: Computer Science/Architecture"
  "date: 2005-12-15"
]
authors: [
  "Solange Coupet-Grimal <Solange.Coupet@lif.univ-mrs.fr> [http://www.cmi.univ-mrs.fr/~solange/]"
  "Line Jakubiec-Jamet <Line.Jakubiec@lif.univ-mrs.fr> [http://www.dil.univ-mrs.fr/~jakubiec/]"
]
bug-reports: "https://github.com/coq-contribs/fairisle/issues"
dev-repo: "git+https://github.com/coq-contribs/fairisle.git"
synopsis: "Proof of the Fairisle 4x4 Switch Element"
description: """
This library contains the development of general definitions dedicated
to the verification of sequential synchronous devices (based on Moore and Mealy automata)
and the formal verification of the Fairisle 4x4 Switch Element."""
flags: light-uninstall
url {
  src: "https://github.com/coq-contribs/fairisle/archive/v8.10.0.tar.gz"
  checksum: "md5=142a12108f624a7e8ee8c9a3b7cc1ae2"
}

Lint

Command
true
Return code
0

Dry install

Dry install with the current Coq version:

Command
opam install -y --show-action coq-fairisle.8.10.0 coq.8.10.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 2h opam install -y --deps-only coq-fairisle.8.10.0 coq.8.10.0
Return code
0
Duration
5 s

Install

Command
opam list; echo; ulimit -Sv 16000000; timeout 2h opam install -y -v coq-fairisle.8.10.0 coq.8.10.0
Return code
0
Duration
1 m 26 s

Installation size

Total: 5 M

  • 389 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Fairisle/PROOFS/Invariant_a4_S.glob
  • 194 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Fairisle/SPECIF/ROUND_ROBIN/Lemmas_on_fcts.glob
  • 173 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Fairisle/PROOFS/Invariant_a4_S.vo
  • 126 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Fairisle/PROOFS/Arbiter4_Proof.vo
  • 117 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Fairisle/PROOFS/Lemmas_Comb_Behaviour.glob
  • 84 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Fairisle/PROOFS/Arbitration_Proof.vo
  • 83 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Fairisle/PROOFS/Lemmas_Comb_Behaviour.vo
  • 81 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Fairisle/SPECIF/ROUND_ROBIN/Lemmas_on_fcts.vo
  • 80 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Fairisle/SPECIF/ELEMENT/ElementTemp.vo
  • 79 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Libraries/Lib_Lists/Fixed_dLists.vo
  • 72 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Libraries/Lib_Lists/Fixed_dLists.glob
  • 71 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Libraries/Lib_Automata/Lemmas_on_Basic_rules.glob
  • 71 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Fairisle/PROOFS/Timing_Arbiter.glob
  • 69 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Fairisle/SPECIF/ELEMENT/Arbitration.vo
  • 65 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Libraries/Lib_Lists/Infinite_lists.vo
  • 62 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Fairisle/PROOFS/Invariant_a4_S.v
  • 62 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Fairisle/PROOFS/Timing_Arbiter.vo
  • 61 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Fairisle/SPECIF/GATES_AND_LATCHES/Lemmas_Struct.vo
  • 57 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Fairisle/SPECIF/ELEMENT/ElementTemp.glob
  • 57 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Libraries/Lib_Lists/Infinite_lists.glob
  • 53 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Libraries/Lib_Automata/Lemmas_on_Basic_rules.vo
  • 53 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Fairisle/PROOFS/Arbitration_beh_sc.vo
  • 51 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Fairisle/PROOFS/Equiv_Struct_Beh_Arbitration.glob
  • 50 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Fairisle/PROOFS/Arbitration_Specif.vo
  • 49 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Fairisle/PROOFS/Arbiter4_Specif.vo
  • 49 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Libraries/Lib_Lists/Dependent_lists_Compl.vo
  • 46 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Fairisle/PROOFS/Equiv_Struct_Beh_Arbitration.vo
  • 46 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Fairisle/PROOFS/Timing_Proof.vo
  • 45 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Libraries/Lib_Automata/Mealy.vo
  • 45 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Fairisle/PROOFS/Arbiter4_Proof_lemmas.vo
  • 44 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Fairisle/SPECIF/GATES_AND_LATCHES/Lemmas_Struct.glob
  • 44 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Fairisle/PROOFS/Lemmas_for_Arbitration.vo
  • 44 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Libraries/Lib_Automata/Basic_composition_rules.glob
  • 43 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Libraries/Lib_Lists/Dependent_lists.vo
  • 42 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Libraries/Lib_Arithmetic/Lib_Mult.vo
  • 42 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Fairisle/PROOFS/Arbitration_Specif.glob
  • 42 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Libraries/Lib_Arithmetic/Lib_Div_Even_Odd.vo
  • 41 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Libraries/Lib_Automata/Basic_composition_rules.vo
  • 41 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Fairisle/SPECIF/ELEMENT/ElementComb.vo
  • 40 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Fairisle/PROOFS/PriorityDecode_Proof.vo
  • 39 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Libraries/Lib_Lists/Dependent_lists_Compl.glob
  • 39 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Fairisle/SPECIF/ROUND_ROBIN/Lemmas_on_fcts.v
  • 38 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Libraries/Lib_Lists/Proj_lists.vo
  • 37 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Libraries/Lib_Arithmetic/Lib_Div_Even_Odd.glob
  • 37 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Libraries/Lib_Lists/dlist_Compl.vo
  • 37 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Fairisle/SPECIF/ELEMENT/ElementComb_Behaviour.vo
  • 36 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Fairisle/PROOFS/Behaviour_Struct_lemmas.vo
  • 35 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Libraries/Lib_Arithmetic/Lib_Exp.vo
  • 35 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Fairisle/SPECIF/ROUND_ROBIN/PortsCompl.vo
  • 34 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Libraries/Lib_Arithmetic/Lib_Minus.vo
  • 34 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Libraries/Lib_Arithmetic/Compare_Nat.vo
  • 34 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Fairisle/SPECIF/ELEMENT/Arbitration.glob
  • 34 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Fairisle/SPECIF/ELEMENT/Tools_Inf.vo
  • 33 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Libraries/Lib_Lists/Manip_BoolLists.vo
  • 33 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Libraries/Lib_Automata/Mealy.glob
  • 32 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Libraries/Lib_Automata/Derived_composition_rules.vo
  • 31 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Libraries/Lib_Lists/Dependent_lists.glob
  • 31 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Libraries/Lib_Lists/Conversions.vo
  • 31 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Fairisle/PROOFS/Arbiter4_Proof_lemmas.glob
  • 31 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Fairisle/SPECIF/GATES_AND_LATCHES/Gen_Gates_Del.vo
  • 30 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Fairisle/SPECIF/GATES_AND_LATCHES/Base_Struct.vo
  • 30 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Fairisle/PROOFS/Arbiter4_Specif.glob
  • 30 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Fairisle/SPECIF/ELEMENT/ElementTemp_Behaviour.vo
  • 30 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Fairisle/SPECIF/ROUND_ROBIN/PickSuccessfulInput.vo
  • 30 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Libraries/Lib_Arithmetic/Lib_Plus.vo
  • 29 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Libraries/Lib_Lists/Tests_in_d_lists.vo
  • 29 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Libraries/Lib_Automata/Moore_Mealy.vo
  • 29 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Fairisle/SPECIF/ROUND_ROBIN/SuccessfulInput.vo
  • 29 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Libraries/Lib_Arithmetic/Lib_Mult.glob
  • 29 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Libraries/Lib_Boolean/Lib_Bool.vo
  • 28 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Libraries/Lib_Arithmetic/Lib_Pred.vo
  • 28 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Fairisle/SPECIF/ELEMENT/Base_Behaviour.vo
  • 28 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Fairisle/SPECIF/ROUND_ROBIN/RoundRobin.vo
  • 28 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Libraries/Lib_Arithmetic/Arith_Compl.vo
  • 27 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Libraries/Lib_Automata/Moore.vo
  • 27 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Fairisle/PROOFS/Lemmas_for_Arbitration.glob
  • 27 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Libraries/Lib_Lists/Lists_of_lists.vo
  • 27 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Libraries/Lib_Boolean/Lib_Zerob.vo
  • 27 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Libraries/Lib_Arithmetic/Lib_Square.vo
  • 27 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Libraries/Lib_Automata/Identity.vo
  • 26 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Fairisle/SPECIF/GATES_AND_LATCHES/Gates_Del.vo
  • 26 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Fairisle/SPECIF/ROUND_ROBIN/NextPort.vo
  • 26 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Libraries/Lib_Lists/PolyList_dlist.vo
  • 26 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Libraries/Lib_Arithmetic/Lib_Eq_Le_Lt.vo
  • 25 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Libraries/Lib_Arithmetic/Lib_Dec.vo
  • 25 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Fairisle/SPECIF/ELEMENT/ElementComb.glob
  • 24 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Libraries/Lib_Automata/Moore_Mealy.glob
  • 23 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Libraries/Lib_Arithmetic/Lib_Fact.vo
  • 21 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Fairisle/PROOFS/Lemmas_Comb_Behaviour.v
  • 20 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Libraries/Lib_Lists/dlist_Compl.glob
  • 18 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Libraries/Lib_Arithmetic/Syntactic_Def.vo
  • 18 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Libraries/Lib_Arithmetic/Compare_Nat.glob
  • 16 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Libraries/Lib_Automata/Derived_composition_rules.glob
  • 16 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Libraries/Lib_Lists/Fixed_dLists.v
  • 15 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Fairisle/SPECIF/ELEMENT/ElementComb_Behaviour.glob
  • 15 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Fairisle/PROOFS/Arbitration_beh_sc.glob
  • 14 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Fairisle/PROOFS/Arbiter4_Proof.glob
  • 14 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Fairisle/PROOFS/Timing_Arbiter.v
  • 14 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Fairisle/SPECIF/ROUND_ROBIN/PortsCompl.glob
  • 14 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Fairisle/PROOFS/Timing_Proof.glob
  • 14 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Libraries/Lib_Arithmetic/Lib_Minus.glob
  • 14 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Libraries/Lib_Lists/Proj_lists.glob
  • 13 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Fairisle/PROOFS/Behaviour_Struct_lemmas.glob
  • 13 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Libraries/Lib_Arithmetic/Lib_Exp.glob
  • 12 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Libraries/Lib_Automata/Lemmas_on_Basic_rules.v
  • 12 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Fairisle/SPECIF/ELEMENT/ElementTemp.v
  • 12 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Libraries/Lib_Lists/Infinite_lists.v
  • 12 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Fairisle/SPECIF/GATES_AND_LATCHES/Gen_Gates_Del.glob
  • 12 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Fairisle/PROOFS/Arbiter4_Proof.v
  • 12 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Fairisle/PROOFS/PriorityDecode_Proof.glob
  • 11 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Libraries/Lib_Boolean/Lib_Bool.glob
  • 10 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Fairisle/PROOFS/Arbitration_Proof.glob
  • 10 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Libraries/Lib_Lists/Manip_BoolLists.glob
  • 10 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Libraries/Lib_Automata/Basic_composition_rules.v
  • 9 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Libraries/Lib_Lists/Dependent_lists_Compl.v
  • 9 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Fairisle/SPECIF/GATES_AND_LATCHES/Gates.glob
  • 9 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Libraries/Lib_Arithmetic/Arith_Compl.glob
  • 9 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Fairisle/SPECIF/GATES_AND_LATCHES/Gates.vo
  • 9 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Libraries/Lib_Arithmetic/Lib_Div_Even_Odd.v
  • 9 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Fairisle/SPECIF/ELEMENT/Arbitration.v
  • 8 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Fairisle/SPECIF/ELEMENT/Tools_Inf.glob
  • 8 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Libraries/Lib_Automata/Mealy.v
  • 8 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Fairisle/SPECIF/GATES_AND_LATCHES/Lemmas_Struct.v
  • 8 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Libraries/Lib_Arithmetic/Lib_Plus.glob
  • 8 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Fairisle/PROOFS/Equiv_Struct_Beh_Arbitration.v
  • 8 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Libraries/Lib_Basis/Lib_Prop.vo
  • 8 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Libraries/Lib_Basis/Lib_Prop.glob
  • 7 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Fairisle/PROOFS/Timing_Proof.v
  • 7 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Libraries/Lib_Arithmetic/Lib_Mult.v
  • 7 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Libraries/Lib_Automata/Moore.glob
  • 7 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Fairisle/PROOFS/Arbitration_Proof.v
  • 7 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Fairisle/PROOFS/Arbitration_Specif.v
  • 7 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Libraries/Lib_Basis/Lib_Set_Products.vo
  • 7 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Fairisle/SPECIF/ELEMENT/ElementTemp_Behaviour.glob
  • 7 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Fairisle/PROOFS/Arbiter4_Specif.v
  • 7 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Fairisle/PROOFS/Arbiter4_Proof_lemmas.v
  • 7 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Libraries/Lib_Lists/Tests_in_d_lists.glob
  • 7 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Libraries/Lib_Automata/Moore_Mealy.v
  • 6 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Libraries/Lib_Boolean/Bool_Compl.glob
  • 6 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Libraries/Lib_Lists/Dependent_lists.v
  • 6 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Libraries/Lib_Boolean/Lib_Zerob.glob
  • 6 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Libraries/Lib_Lists/PolyList_dlist.glob
  • 6 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Fairisle/PROOFS/Lemmas_for_Arbitration.v
  • 6 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Libraries/Lib_Arithmetic/Lib_Pred.glob
  • 6 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Fairisle/SPECIF/ELEMENT/ElementComb.v
  • 6 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Libraries/Lib_Lists/dlist_Compl.v
  • 6 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Libraries/Lib_Basis/Lib_Set_Products.glob
  • 6 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Libraries/Lib_Boolean/Bool_Compl.vo
  • 6 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Libraries/Lib_Arithmetic/Compare_Nat.v
  • 6 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Libraries/Lib_Lists/Lists_of_lists.glob
  • 5 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Libraries/Lib_Lists/Conversions.glob
  • 5 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Fairisle/SPECIF/ROUND_ROBIN/PortsCompl.v
  • 5 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Fairisle/SPECIF/ELEMENT/ElementComb_Behaviour.v
  • 5 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Fairisle/PROOFS/PriorityDecode_Proof.v
  • 5 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Libraries/Lib_Arithmetic/Lib_Exp.v
  • 5 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Libraries/Lib_Basis/Product.glob
  • 5 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Libraries/Lib_Arithmetic/Syntactic_Def.glob
  • 5 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Libraries/Lib_Arithmetic/Lib_Minus.v
  • 5 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Libraries/Lib_Lists/Proj_lists.v
  • 5 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Fairisle/PROOFS/Arbitration_beh_sc.v
  • 5 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Libraries/Lib_Arithmetic/Lib_Square.glob
  • 5 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Fairisle/SPECIF/ELEMENT/Base_Behaviour.glob
  • 5 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Libraries/Lib_Automata/Derived_composition_rules.v
  • 5 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Libraries/Lib_Basis/Product.vo
  • 5 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Fairisle/SPECIF/GATES_AND_LATCHES/Base_Struct.glob
  • 4 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Fairisle/SPECIF/ROUND_ROBIN/SuccessfulInput.glob
  • 4 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Libraries/Lib_Arithmetic/Lib_Dec.glob
  • 4 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Libraries/Lib_Arithmetic/Syntactic_Def.v
  • 4 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Fairisle/PROOFS/Behaviour_Struct_lemmas.v
  • 4 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Fairisle/SPECIF/ELEMENT/Tools_Inf.v
  • 4 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Libraries/Lib_Lists/Tests_in_d_lists.v
  • 4 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Libraries/Lib_Lists/Manip_BoolLists.v
  • 4 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Libraries/Lib_Arithmetic/Lib_Eq_Le_Lt.glob
  • 4 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Fairisle/SPECIF/ROUND_ROBIN/PickSuccessfulInput.glob
  • 4 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Libraries/Lib_Boolean/Lib_Bool.v
  • 4 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Fairisle/SPECIF/ROUND_ROBIN/RoundRobin.glob
  • 4 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Libraries/Lib_Arithmetic/Lib_Plus.v
  • 3 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Libraries/Lib_Lists/Conversions.v
  • 3 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Libraries/Lib_Arithmetic/Arith_Compl.v
  • 3 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Libraries/Lib_Basis/Lib_Prop.v
  • 3 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Fairisle/SPECIF/GATES_AND_LATCHES/Gates.v
  • 3 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Libraries/Lib_Boolean/Lib_Zerob.v
  • 3 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Fairisle/SPECIF/GATES_AND_LATCHES/Gen_Gates_Del.v
  • 3 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Libraries/Lib_Automata/Moore.v
  • 3 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Libraries/Lib_Arithmetic/Lib_Pred.v
  • 3 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Libraries/Lib_Automata/Identity.glob
  • 3 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Libraries/Lib_Boolean/Bool_Compl.v
  • 3 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Libraries/Lib_Lists/Lists_of_lists.v
  • 3 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Fairisle/SPECIF/ROUND_ROBIN/SuccessfulInput.v
  • 3 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Libraries/Lib_Lists/PolyList_dlist.v
  • 3 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Libraries/Lib_Automata/Identity.v
  • 3 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Fairisle/SPECIF/ELEMENT/ElementTemp_Behaviour.v
  • 3 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Libraries/Lib_Basis/Lib_Set_Products.v
  • 3 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Fairisle/SPECIF/ROUND_ROBIN/NextPort.glob
  • 3 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Libraries/Lib_Arithmetic/Lib_Square.v
  • 3 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Fairisle/SPECIF/ROUND_ROBIN/PickSuccessfulInput.v
  • 3 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Fairisle/SPECIF/ROUND_ROBIN/RoundRobin.v
  • 3 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Libraries/Lib_Arithmetic/Lib_Dec.v
  • 3 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Libraries/Lib_Arithmetic/Lib_Eq_Le_Lt.v
  • 3 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Fairisle/SPECIF/GATES_AND_LATCHES/Base_Struct.v
  • 3 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Fairisle/SPECIF/ELEMENT/Base_Behaviour.v
  • 3 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Fairisle/SPECIF/ROUND_ROBIN/NextPort.v
  • 3 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Fairisle/SPECIF/GATES_AND_LATCHES/Gates_Del.glob
  • 3 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Libraries/Lib_Basis/Product.v
  • 2 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Libraries/Lib_Basis/Injections.vo
  • 2 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Fairisle/SPECIF/GATES_AND_LATCHES/Gates_Del.v
  • 2 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Fairisle/SPECIF/ROUND_ROBIN/TypePorts.v
  • 2 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Libraries/Lib_Basis/Injections.v
  • 2 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Libraries/Lib_Arithmetic/Lib_Fact.v
  • 2 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Fairisle/SPECIF/ROUND_ROBIN/TypePorts.vo
  • 2 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Libraries/Lib_Basis/Injections.glob
  • 1 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Fairisle/SPECIF/ROUND_ROBIN/TypePorts.glob
  • 1 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Fairisle/Libraries/Lib_Arithmetic/Lib_Fact.glob

Uninstall

Command
opam remove -y coq-fairisle.8.10.0
Return code
0
Missing removes
none
Wrong removes
none

Sources are on GitHub. © Guillaume Claret.