SSReflect 및 MathComp를 Linux에 설치하는 방법은 무엇입니까?

Question

나는 Coq 8.6과 CoqIDE를 리눅스 (우분투 17.04)에 성공적으로 설치했다. 그러나 SSReflect 및 MathComp를이 설치에 추가하기 위해 계속 진행할 필요는 없습니다. 내가 확인한 모든 참고 문헌들은 나에게 매우 혼란스러워 보였다. 누구든지 똑바로 간단하게 그 요리법을 가지고 있습니까? 나는 opam을 설치했다.

Answer 1

나는 우분투 16.04에 있습니다. 이제 다시 걸음을하고 OPAM를 설치하여 시작하자 :

$ sudo apt update && sudo apt install opam 
$ opam --version 
1.2.2 
$ opam init  # agree to modify your dot-files 
$ eval `opam config env` 
$ ocamlc -version 
4.02.3 

다음으로, 좀 더 최근의 우분투의 꽤 오래된 OCaml의 버전으로 전환 할 수 있습니다. 이 단계는 선택 사항이며 약 10 분이 소요됩니다. 이제

$ opam switch 4.04.1 
$ eval `opam config env` 
$ ocamlc -version 
4.04.1 

,의 수학 - 완 설치 할 수 있도록 다음 저장소를 추가 할 수 있습니다 :

$ opam install coq-mathcomp-ssreflect 

OPAM가 종속성을 파악합니다 : 마지막으로,

$ opam repo add coq-released https://coq.inria.fr/opam/released 

을 그리고, ssreflect 설치 (Coq 포함), 우리가 요청한 것을 다운로드하여 설치하십시오!

Answer 2

OPAM 대신 the Nix package manager을 사용하여 다른 방법을 사용할 수 있습니다. 그것은 (curl https://nixos.org/nix/install | sh)을 설치 한 후 다음 명령을 사용하여 수학 - 경화제와 CoqIDE 사용할 수를 실행할 수 있습니다 :

는

nix-shell -p coqPackages_8_6.mathcomp --run coqide 

그럼 그냥`opam이 COQ-mathcomp-ssreflect를 설치 하는가 From mathcomp Require Import ssreflect.