10000 Add support for installing system packages · Issue #6 · vzaliva/coq-config · GitHub
[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to content

Add support for installing system packages #6

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
zoickx opened this issue Sep 7, 2021 · 1 comment
Open

Add support for installing system packages #6

zoickx opened this issue Sep 7, 2021 · 1 comment

Comments

@zoickx
Copy link
zoickx commented Sep 7, 2021

Some opam packages have system non-OCaml dependencies, managed by the system's package manager.
As of now, coq-config will fail to install such dependencies, despite them being supported by default with opam depext since 2.1.0.
See more in opam FAQ, GitHub repo.

@zoickx
Copy link
Author
zoickx commented Sep 7, 2021

An example of a failed invocation looks like this (no user input)

$ coq-config

<><> Installing new switch packages <><><><><><><><><><><><><><><><><><><><><><>
Switch invariant: ["ocaml-base-compiler" {= "4.12.0"} | "ocaml-system" {= "4.12.0"}]

<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
-> installed base-bigarray.base
-> installed base-threads.base
-> installed base-unix.base
-> installed ocaml-options-vanilla.1
-> retrieved ocaml-base-compiler.4.12.0  (https://opam.ocaml.org/cache)
-> installed ocaml-base-compiler.4.12.0
-> installed ocaml-config.2
-> installed ocaml.4.12.0
Done.
# Run eval $(opam env --switch=asn1-vst28) to update the current shell environment
[coq-released] Initialised
coq-vst-32 is now pinned to version 2.8
Package coq-struct-tact does not exist, create as a NEW package? [Y/n] y
[coq-struct-tact.~dev] synchronised (git+https://github.com/uwplse/StructTact.git)
coq-struct-tact is now pinned to git+https://github.com/uwplse/StructTact.git (version dev)

<><> Synchronising pinned packages ><><><><><><><><><><><><><><><><><><><><><><>
[coq-struct-tact.dev] synchronised (no changes)

The following actions will be performed:
  - install ocamlfind       1.9.1    [required by coq]
  - install conf-g++        1.0      [required by coq-flocq]
  - install conf-gmp        3        [required by zarith]
  - install conf-findutils  1        [required by coq]
  - install dune            2.9.0    [required by coq-struct-tact]
  - install num             1.4      [required by coq]
  - install zarith          1.12     [required by coq]
  - install menhirSdk       20210419 [required by menhir]
  - install menhirLib       20210419 [required by menhir]
  - install coq             8.13.2   [required by coq-struct-tact, coq-ext-lib, coq-vst-32]
  - install menhir          20210419 [required by coq-compcert-32]
  - install coq-struct-tact dev*
  - install coq-menhirlib   20210419 [required by coq-compcert-32]
  - install coq-flocq       3.4.2    [required by coq-vst-32]
  - install coq-ext-lib     0.11.3
  - install coq-compcert-32 3.9      [required by coq-vst-32]
  - install coq-vst-32      2.8*
===== 17 to install =====

The following system packages will first need to be installed:
    libgmp-dev


<><> Handling external dependencies <><><><><><><><><><><><><><><><><><><><><><>
Let opam run your package manager to install the required system packages?
(answer 'n' for other options) [Y/n] n
This command should get the requirements installed:

    apt-get install libgmp-dev

[NOTE] Use 'opam option depext-run-installs=false' if you don't want to be prompted again.
You can retry with '--assume-depexts' to skip this check, or run 'opam option depext=false' to permanently disable handling of system packages altogether.
Error installing pakages

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant
0