~amiloradovsky/symbolic-dynamics

symbolic-dynamics/README.org -rw-r--r-- 1.2 KiB View raw
5857f238Andrew Miloradovsky .build.yml: continuous integration for SourceHut 7 months ago
                                                                                
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
* Dependencies

  The topology library by Daniel Schepler:

  - https://github.com/coq-community/topology
  - https://github.com/coq-community/zorns-lemma

  These may be installed from OPAM by [fn:SE]:

  #+BEGIN_SRC shell
  opam repo add coq-released https://coq.inria.fr/opam/released
  opam update
  opam upgrade  # if possible, for Dune
  opam install coq-topology
  #+END_SRC

  Or (better) from the sources (see below).

* Building fresh version from VCS

  #+BEGIN_SRC shell
  git clone git@github.com:coq-community/zorns-lemma.git
  cd zorns-lemma
  make all
  cd ..
  #+END_SRC

  #+BEGIN_SRC shell
  git clone git@github.com:coq-community/topology.git
  cd topology
  sed -i '2s@^$@-R ../zorns-lemma ZornsLemma@' Make  # set the real path
  make all
  ln -s Make _CoqProject  # for ProofGeneral to see the real paths
  cd ..
  #+END_SRC

  #+BEGIN_SRC shell
  git clone git@gitlab.com:symbolic-dynamics/symbolic-dynamics.git
  cd symbolic-dynamics
  coq_makefile -f _CoqProject -o Makefile
  make all
  #+END_SRC

  The real paths for the dependencies are already specified in ~_CoqProject~ as above,
  change them, if you have a different directory hierarchy.

* Footnotes

[fn:SE] https://stackoverflow.com/questions/49602587/installing-packages-for-coq-using-opam