Created
August 4, 2020 13:03
-
-
Save pirapira/737f0b8ba2e3e94ba85c8d1f67bdbd0d to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| privat@yoichi-MS-7A93:~/shared/cpp2v$ coq --version | |
| Command 'coq' not found, did you mean: | |
| command 'oq' from snap oq (1.1.2) | |
| command 'coz' from deb coz-profiler (0.1.0-2ubuntu3) | |
| command 'cow' from deb fl-cow (0.6-4.2) | |
| command 'cnq' from deb cplay (1.50-2) | |
| command 'col' from deb bsdmainutils (11.1.2ubuntu3) | |
| command 'coqc' from deb coq (8.11.0-1) | |
| command 'cog' from deb cog (0.4.0-2) | |
| command 'co' from deb rcs (5.9.4-6) | |
| See 'snap info <snapname>' for additional versions. | |
| privat@yoichi-MS-7A93:~/shared/cpp2v$ coqc --version | |
| The Coq Proof Assistant, version 8.11.0 (August 2020) | |
| compiled on Aug 3 2020 19:42:23 with OCaml 4.08.1 | |
| privat@yoichi-MS-7A93:~/shared/cpp2v$ opam list | |
| # Packages matching: installed | |
| # Name # Installed # Synopsis | |
| async v0.13.0 Monadic concurrency library | |
| async_kernel v0.13.0 Monadic concurrency library | |
| async_rpc_kernel v0.13.0 Platform-independent core of Async RPC l | |
| async_unix v0.13.0 Monadic concurrency library | |
| base v0.13.2 Full standard library replacement for OC | |
| base-bigarray base | |
| base-bytes base Bytes library distributed with the OCaml | |
| base-threads base | |
| base-unix base | |
| base64 3.4.0 Base64 encoding for OCaml | |
| base_bigstring v0.13.0 String type based on [Bigarray], for use | |
| base_quickcheck v0.13.0 Randomized testing framework, designed f | |
| bigarray-compat 1.0.0 Compatibility library to use Stdlib.Biga | |
| bignum v0.13.0 Core-flavoured wrapper around zarith's a | |
| bin_prot v0.13.0 A binary protocol generator | |
| biniou 1.2.1 Binary data format designed for speed, s | |
| bisect_ppx 2.4.1 Code coverage for OCaml | |
| cmdliner 1.0.4 Declarative definition of command line i | |
| conf-findutils 1 Virtual package relying on findutils | |
| conf-gmp 1 Virtual package relying on a GMP lib sys | |
| conf-m4 1 Virtual package relying on m4 | |
| conf-perl 1 Virtual package relying on perl | |
| conf-pkg-config 1.2 Virtual package relying on pkg-config in | |
| coq 8.11.0 pinned to version 8.11.0 | |
| coq-equations 1.2.3+8.11 A function definition package for Coq | |
| coq-ext-lib 0.11.1 A library of Coq definitions, theorems, | |
| coq-iris 3.3.0 Iris is a Higher-Order Concurrent Separa | |
| coq-iris-string-ident dev Add support for Gallina names in intro p | |
| coq-lens 1.0.0 Generation of lenses for record datatype | |
| coq-metacoq-template 1.0~alpha2+8.11 A quoting and unquoting library for Coq | |
| coq-stdpp 1.4.0 std++ is an extended "Standard Library" | |
| core v0.13.0 Industrial strength alternative to OCaml | |
| core_kernel v0.13.1 Industrial strength alternative to OCaml | |
| cppo 1.6.6 Code preprocessor like cpp for OCaml | |
| ctypes 0.17.1 Combinators for binding to C libraries w | |
| digestif 0.8.0-1 Hashes implementations (SHA*, RIPEMD160, | |
| dune 2.5.1 Fast, portable, and opinionated build sy | |
| dune-configurator 2.5.1 Helper library for gathering system conf | |
| dune-private-libs 2.5.1 Private libraries of Dune | |
| easy-format 1.3.2 High-level and functional interface to t | |
| eqaf 0.7 Constant-time equal function on string | |
| fieldslib v0.13.0 Syntax extension to define first class v | |
| integers 0.4.0 Various signed and unsigned integer type | |
| jane-street-headers v0.13.0 Jane Street C header files | |
| jst-config v0.13.0 Compile-time configuration for Jane Stre | |
| menhir 20200211 An LR(1) parser generator | |
| menhirLib 20200211 Runtime support library for parsers gene | |
| menhirSdk 20200211 Compile-time library for auxiliary tools | |
| num 1.3 The legacy Num library for arbitrary-pre | |
| ocaml 4.08.1 The OCaml compiler (virtual package) | |
| ocaml-compiler-libs v0.12.1 OCaml compiler libraries repackaged | |
| ocaml-config 1 OCaml Switch Configuration | |
| ocaml-migrate-parsetree 1.7.3 Convert OCaml parsetrees between differe | |
| ocaml-system 4.08.1 The OCaml compiler (system version, from | |
| ocamlfind 1.8.1 A library manager for OCaml | |
| octavius 1.2.2 Ocamldoc comment syntax parser | |
| parsexp v0.13.0 S-expression parsing library | |
| ppx_assert v0.13.0 Assert-like extension nodes that raise u | |
| ppx_base v0.13.0 Base set of ppx rewriters | |
| ppx_bench v0.13.0 Syntax extension for writing in-line ben | |
| ppx_bin_prot v0.13.0 Generation of bin_prot readers and write | |
| ppx_cold v0.13.0 Expands [@cold] into [@inline never][@sp | |
| ppx_compare v0.13.0 Generation of comparison functions from | |
| ppx_custom_printf v0.13.0 Printf-style format-strings for user-def | |
| ppx_derivers 1.2.1 Shared [@@deriving] plugin registry | |
| ppx_deriving 4.4.1 Type-driven code generation for OCaml >= | |
| ppx_deriving_yojson 3.5.2 JSON codec generator for OCaml | |
| ppx_enumerate v0.13.0 Generate a list containing all values of | |
| ppx_expect v0.13.1 Cram like framework for OCaml | |
| ppx_fail v0.13.0 Add location to calls to failwiths | |
| ppx_fields_conv v0.13.0 Generation of accessor and iteration fun | |
| ppx_hash v0.13.0 A ppx rewriter that generates hash funct | |
| ppx_here v0.13.0 Expands [%here] into its location | |
| ppx_inline_test v0.13.1 Syntax extension for writing in-line tes | |
| ppx_jane v0.13.0 Standard Jane Street ppx rewriters | |
| ppx_js_style v0.13.0 Code style checker for Jane Street Packa | |
| ppx_let v0.13.0 Monadic let-bindings | |
| ppx_module_timer v0.13.0 Ppx rewriter that records top-level modu | |
| ppx_optcomp v0.13.0 Optional compilation for OCaml | |
| ppx_optional v0.13.0 Pattern matching on flat options | |
| ppx_pipebang v0.13.0 A ppx rewriter that inlines reverse appl | |
| ppx_sexp_conv v0.13.0 [@@deriving] plugin to generate S-expres | |
| ppx_sexp_message v0.13.0 A ppx rewriter for easy construction of | |
| ppx_sexp_value v0.13.0 A ppx rewriter that simplifies building | |
| ppx_stable v0.13.0 Stable types conversions generator | |
| ppx_tools 6.0+4.08.0 Tools for authors of ppx rewriters and o | |
| ppx_tools_versioned 5.4.0 A variant of ppx_tools based on ocaml-mi | |
| ppx_typerep_conv v0.13.0 Generation of runtime types from type de | |
| ppx_variants_conv v0.13.0 Generation of accessor and iteration fun | |
| ppxfind 1.4 Tool combining ocamlfind and ppx | |
| ppxlib 0.13.0 Base library and tools for ppx rewriters | |
| protocol_version_header v0.13.0 Protocol versioning | |
| re 1.9.0 RE is a regular expression library for O | |
| result 1.5 Compatibility Result module | |
| seq base Compatibility package for OCaml's standa | |
| sexplib v0.13.0 Library for serializing OCaml values to | |
| sexplib0 v0.13.0 Library containing the definition of S-e | |
| spawn v0.13.0 Spawning sub-processes | |
| splittable_random v0.13.0 PRNG that can be split into independent | |
| stdio v0.13.0 Standard IO library for OCaml | |
| stdlib-shims 0.1.0 Backport some of the new stdlib features | |
| textutils v0.13.0 Text output utilities | |
| time_now v0.13.0 Reports the current time | |
| typerep v0.13.0 Typerep is a library for runtime types | |
| variantslib v0.13.0 Part of Jane Street's Core library | |
| yojson 1.7.0 Yojson is an optimized parsing and print | |
| zarith 1.9.1 Implements arithmetic and logical operat | |
| zarith_stubs_js v0.13.0 Javascripts stubs for the Zarith library |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment