# Packages matching: installed # Name # Installed # Synopsis base-bigarray base base-threads base base-unix base camlp5 7.14 Preprocessor-pretty-printer of OCaml conf-findutils 1 Virtual package relying on findutils conf-perl 2 Virtual package relying on perl coq 8.9.0 Formal proof management system num 1.4 The legacy Num library for arbitrary-precision integer and rational arithmetic ocaml 4.09.1 The OCaml compiler (virtual package) ocaml-base-compiler 4.09.1 Official release 4.09.1 ocaml-config 1 OCaml Switch Configuration ocamlfind 1.9.3 A library manager for OCaml # opam file: opam-version: "2.0" maintainer: "Hugo.Herbelin@inria.fr" homepage: "https://github.com/coq-contribs/pautomata" license: "LGPL 2.1" build: [make "-j%{jobs}%"] install: [make "install"] remove: ["rm" "-R" "%{lib}%/coq/user-contrib/PAutomata"] depends: [ "ocaml" "coq" {>= "8.9" & < "8.10~"} ] tags: [ "keyword: p-automata" "keyword: ABR" "keyword: PGM" "keyword: time" "category: Computer Science/Concurrent Systems and Protocols/Theory of concurrent systems" ] authors: [ "Emmanuel Freund & Christine Paulin" ] bug-reports: "https://github.com/coq-contribs/pautomata/issues" dev-repo: "git+https://github.com/coq-contribs/pautomata.git" synopsis: "Parameterized automata" description: """ This contribution is a modelisation in Coq of the p-automata designed in the CALIFE project (http://www.loria.fr/calife). It contains an axiomatisation of time, the definition of a p-automaton, the definition of binary and arbitrary synchronisation of a family of p-automaton, the semantics of a p-automaton as a labelled transition system. The description of the ABR algorithm as a p-automaton is also given. This work is reported in : P. Castéran, E. Freund, C. Paulin and D. Rouillard ``Bibliothèques Coq et Isabelle-HOL pour les systèmes de transitions et les p-automates''""" flags: light-uninstall url { src: "https://github.com/coq-contribs/pautomata/archive/v8.9.0.tar.gz" checksum: "md5=ac22083aa7f43752637891ba0ab5f1d4" }
true
Dry install with the current Coq version:
opam install -y --show-action coq-pautomata.8.9.0 coq.8.9.0
Dry install without Coq/switch base, to test if the problem was incompatibility with the current Coq/OCaml version:
true
opam list; echo; ulimit -Sv 4000000; timeout 4h opam install -y --deps-only coq-pautomata.8.9.0 coq.8.9.0
opam list; echo; ulimit -Sv 16000000; timeout 4h opam install -y -v coq-pautomata.8.9.0 coq.8.9.0
Total: 2 M
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/PAutomata/PGM/Pgm.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/PAutomata/PGM/Pgm.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/PAutomata/ABRgen.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/PAutomata/Evenements.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/PAutomata/ABRgen.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/PAutomata/PAutomataMod.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/PAutomata/Timebase.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/PAutomata/ABRdef.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/PAutomata/PGM/Vpauto.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/PAutomata/Timebase.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/PAutomata/AutoLMod.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/PAutomata/PAutomata.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/PAutomata/gCSMA_CD/Sender.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/PAutomata/gCSMA_CD/Contexte.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/PAutomata/Properties.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/PAutomata/PGM/Vpauto.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/PAutomata/gCSMA_CD/Bus.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/PAutomata/gCSMA_CD/Block_gCSMA_CD.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/PAutomata/GAutomata.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/PAutomata/PGM/Pgm.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/PAutomata/ABRdef.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/PAutomata/AutoL.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/PAutomata/Time.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/PAutomata/ABRgen.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/PAutomata/PGM/Queue.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/PAutomata/Transitions.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/PAutomata/PGM/String.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/PAutomata/gCSMA_CD/Sender.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/PAutomata/PAutomataMod.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/PAutomata/PGAuto.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/PAutomata/Evenements.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/PAutomata/TimeSyntax.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/PAutomata/PAutoMod.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/PAutomata/PAuto.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/PAutomata/Coercions.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/PAutomata/Extract.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/PAutomata/Transitions.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/PAutomata/TransMod.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/PAutomata/PAutomata.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/PAutomata/GAutomata.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/PAutomata/TransMod.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/PAutomata/LList.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/PAutomata/PGM/Map.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/PAutomata/PGM/Var.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/PAutomata/Timebase.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/PAutomata/AutoLMod.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/PAutomata/PGM/Vpauto.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/PAutomata/gCSMA_CD/Bus.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/PAutomata/LList.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/PAutomata/PGM/Var.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/PAutomata/PAutomataMod.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/PAutomata/gCSMA_CD/preambule.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/PAutomata/Properties.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/PAutomata/ABRdef.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/PAutomata/Time.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/PAutomata/Evenements.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/PAutomata/GAutomata.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/PAutomata/PAutomata.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/PAutomata/TransMod.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/PAutomata/gCSMA_CD/Block_gCSMA_CD.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/PAutomata/Transitions.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/PAutomata/PGM/String.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/PAutomata/PGM/Var.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/PAutomata/AutoL.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/PAutomata/PGM/Queue.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/PAutomata/AutoLMod.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/PAutomata/Properties.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/PAutomata/PGM/Map.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/PAutomata/gCSMA_CD/Sender.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/PAutomata/Time.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/PAutomata/LList.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/PAutomata/Trace.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/PAutomata/PGM/Queue.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/PAutomata/gCSMA_CD/Bus.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/PAutomata/PGM/Map.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/PAutomata/AutoL.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/PAutomata/gCSMA_CD/Block_gCSMA_CD.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/PAutomata/PGM/String.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/PAutomata/Trace.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/PAutomata/PGAuto.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/PAutomata/PGM/Comp.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/PAutomata/gCSMA_CD/Contexte.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/PAutomata/Trace.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/PAutomata/PGM/Comp.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/PAutomata/PGAuto.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/PAutomata/PAutoMod.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/PAutomata/PAuto.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/PAutomata/Extract.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/PAutomata/TimeSyntax.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/PAutomata/gCSMA_CD/Contexte.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/PAutomata/gCSMA_CD/preambule.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/PAutomata/Coercions.v
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/PAutomata/PGM/Comp.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/PAutomata/gCSMA_CD/preambule.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/PAutomata/TimeSyntax.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/PAutomata/PAutoMod.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/PAutomata/PAuto.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/PAutomata/Coercions.glob
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/PAutomata/Extract.glob
opam remove -y coq-pautomata.8.9.0