Skip to content

Latest commit

 

History

History
202 lines (187 loc) · 9.38 KB

install-windows-en.org

File metadata and controls

202 lines (187 loc) · 9.38 KB
Raw

Installation of MathComp on Windows 10

We present three ways to install MathComp on Windows 10.

Method 1 relies on Windows Subsystem for Linux. The resulting working environment is reportedly comfortable, but WSL is rather new, and installation takes time. As of today [2021-04-23 Fri], this is however maybe the best compromise.

Method 2 and 3 rely on cygwin to recreate a Linux-like environment. Warning: file access with cygwin is slow compared to a native Linux installation. Method 2 avoids opam completely and uses the binary distribution of Coq for Windows 10 to compile the desired libraries one after the other using make. It is quick, has always worked, but the result can be a bit clunky. Method 3 uses a custom installation of “opam for Windows” (cygwin’s opam does not seem to be usable), it results in a more comfortable working environment, but installation is slow and may fail because opam support for Windows is rather new.

Method 1: WSL 2 + opam

NB: From Windows 10 version 2004, it seems that there is an alternative installation method that is a bit shorter. wsl --install enables virtualization and install the default distribution with the latest kernel

Step 0: Install WSL 2

  • Check the version of Windows 10: type Windows Key + R, execute winver.
    • Upgrade to 1903 if necessary
  • Choose a Linux distribution for WSL (ref):
    1. Execute Windows PowerShell with administrator rights
    2. dism.exe /online /enable-feature /featurename:Microsoft-Windows-Subsystem-Linux /all /norestart
    3. Reboot
    4. Execute Windows PowerShell with administrator rights
    5. dism.exe /online /enable-feature /featurename:VirtualMachinePlatform /all /norestart
    6. Reboot
    7. Download the package for upgrade of the Linux kernel
    8. Fix the version: wsl --set-default-version 2
    9. Download and install a Linux distribution from Microsoft Store
      • Debian GNU/Linux is a safe choice, Ubuntu is fine too
  • Execute Linux from Windows’ Start Menu or the search window
    1. Choose a user name and password
    2. Install basic software using the package manager
      • sudo add-apt-repository ppa:avsm/ppa (Ubuntu only)
      • sudo apt update
      • sudo apt-get install emacs
  • Better to have an Xorg server to use emacs or vscode
    1. download and install VcXsrv
    2. execute VcXsrv using the XLaunch icon
    3. choose the options multiple windows, start no client, and Disable access control
    4. Fix the configuration of Windows 10
      • Open “Firewall and network protection”
      • Click on “Advanced Setting” below “Public network”
      • Open “Inbound rules” for “VcXsrv windows xserver”
      • In “General/Operation”, select “Allo connection”
      • In “Scope”, add “192.168.0.0/162
  • Set the DISPLAY environment variable through WSL’s shell:
    • add export DISPLAY=$(awk '/nameserver / {print $2; exit}' /etc/resolv.conf 2>/dev/null):0 in ./bashrc
    • Start VcXsrv, restart bash, and then emacs should be usable as an independent window

Install opam, Coq, and MathComp

  • Install opam using the package manager of WLS’s Linux distribution:
    1. sudo apt install opam
    2. opam init
      • Don’t worry if it takes time
    3. opam switch create 4.11.2 (or opam switch create ocaml-base-compiler.4.11.2 ?)
      • Takes time
    4. See opam website for other Linux distributions (not based on Debian)
  • opam install coq
    • Current version [2021-04-23 Fri] is 8.13.2
    • Takes time
    • To use development versions [2019-09-24 Tue] (such as beta’s):
      • opam repo add coq-core-dev https://coq.inria.fr/opam/core-dev
      • opam install coq.8.10+beta3
  • You need GTK+ header files to install CoqIDE
    • sudo apt install xyz where xyz is libcairo2-dev, libexpat1-dev, libgtk-3-dev, libgtksourceview-3.0-dev
    • opam install coqide
  • Install MathComp
    • opam repo add coq-released https://coq.inria.fr/opam/released
    • opam install coq-mathcomp-ssreflect, etc.

Methods 2 and 3

Step 0: Install cygwin

  • Download and execute setup-x86_64.exe from https://www.cygwin.com/
    • Choose xinit, make, diffutils, patch, unzip, git, emacs, emacs-X11, vim, texlive to have a minimal working environment
  • Double-click the “Cygwin64 Terminal” on the Desktop
  • In the terminal, execute startxwin to start X11
    • An Cygwin-X11 icon (a black “C” with a green “X” inside) appears among the System Tray icons
    • Right-clicking the Cygwin-X11 icon gives access to xterm
      • You can launch emacs from the command line

Method 2: cygwin + binaries (Install MathComp using the Coq Platform Binaries)

  • Download and execute the Coq Platform from the release page

COMMENT

  • This will add the Coq distribution as the C:\Coq directory
  • Add /cygdrive/c/coq/bin to PATH
    • By appending export PATH=${PATH}:/cygdrive/c/coq/bin/ to .bashrc for example

Method 3: cygwin + opam (Install MathComp using opam)

The following results in a more comfortable working environment but the process is slow and may fail. Still, at least, it should leave you with a working OCaml compiler to compile Coq from the source and go on installing MathComp as in Method 1.

Step 3-a: Install opam

  • For opam to work, add a few more useful programs by re-running the cygwin installer
    • rsync, curl, m4, perl, mingw64-x86_64-gcc-core
  • Download opam
  • tar -xf opam64.tar.xz
  • bash opam64/install.sh
  • opam init default "https://github.com/fdopen/opam-repository-mingw.git#opam2" -c "ocaml-variants.4.07.1+mingw64c" --disable-sandboxing
    • this modifies .bash_profile
  • eval $(opam config env)
  • opam switch create 4.07.1+mingw64c
    • if the right OCaml compiler is not here

Step 3-b: Install Coq

  • opam install camlp5 ([2019-07-12 Fri]’s version: 7.06)
  • opam install ocamlfind ([2019-07-12 Fri]’s version: 1.8.0)
  • opam install depext ([2019-07-12 Fri]’s version: transition)
  • opam install depext-cygwinports ([2019-07-12 Fri]’s version: 0.0.7)
    • Add /usr/x86_64-w64-mingw32/sys-root/mingw/bin to PATH as indicated
  • opam install pcre
    • mail fail partially, but this is no worry because it should not prevent you from installing Coq, MathComp, etc.
  • try opam install lablgtk
    • the complete installation is likely to fail, this means no coqIDE, but this is no problem because there is Proof General
  • opam install num ([2019-07-12 Fri]’s version: 1.2)
  • opam repo add coq-released https://coq.inria.fr/opam/released
  • opam install coq.8.9.1

Step 3-c: Install MathComp

  • export CAML=/home/username/.opam/4.07.1+mingw64c/bin/
  • export COQBIN=/home/username/.opam/4.07.1+mingw64c/bin/
  • opam install coq-mathcomp-ssreflect ([2019-07-12 Fri]’s version: 1.9.0)
  • opam install coq-mathcomp-fingroup
  • opam install coq-mathcomp-algebra
  • opam install coq-mathcomp-field

Install Proof General

  • Install proof general following the instructions online
  • Add this point, you can already use Coq and some version of MathComp almost as if you were on a Linux-based system

Troubleshooting and Failures

Cygwin Troubleshooting

  • Cygwin may be confused by a non-American keyboard; you can change the keyboard layout with setxkbmap, e.g., for a Japanese keyboard, setxkbmap -model jp106 -layout jp
  • You may want to get rid of the CAPS LOCK key by creating a file, say, Xmodmap with the following contents:
keycode 66 = Control_L
clear Lock
add Control = Control_L

Then append the following to .bashrc:

xmodmap /home/username/Xmodmap

Opam Troubleshooting

  • You may witness Device or resource busy when installing with opam, they seem to be harmless
  • opam install lablgtk fails with the following error despite having libgtk2.0-devel and mingw64-x86_64-gtk2.0 installed with cygwin:
This package requires gtk+ 2.0 development packages installed on your system

Cygwin’s opam troubleshooting

Install OCaml with cygwin’s opam on Windows 10

It is possible to install the OCaml compiler using cygwin’s opam (using the procedure below) but the compiler obtained this way cannot be used to compile Coq.

  • Re-run the cygwin installer to install opam (version 2 or higher)
  • opam init (Answer “y” to questions)
  • eval $(opam env)
  • Check that OCaml has been properly installed
    • ocaml --version (version at the time of this writing [2019-07-08 Mon]: 4.04.2)
  • opam switch create 4.07.1
  • eval $(opam env)
  • opam install camlp5 (version 7.06.10 [2019-07-08 Mon])
  • opam install ocamlfind (version 1.8.0 [2019-07-08 Mon])
  • opam install num.1.2

Failure Installing Coq from the source code using cygwin’s opam’s OCaml

Using cygwin’s opam

Installation fails because Coq’s configure is confused by cygwin:

  • opam repo add coq-released https://coq.inria.fr/opam/released
  • opam install coq.8.0.1

From the source, using cygwin’s opam’s Ocaml

Installation fails with an “address space is already occupied error” for dllunix.so:

  • Download coq.8.9.1.tar.gz
  • unzip, untar, cd, make