Installation

Frama-C depends on OCaml and ocamlfind (findlib), a separate product that builds by default into /util/bin.

---

Alt-Ergo:    http://alt-ergo.ocamlpro.com

  depends on camlp4
% cd camlp4-4.02/
% ./configure
%  make
% sudo make install

  depends on gtksourceview


  depends on lablgtk
% cd lablgtk-2.18.3
% ./configure
% make
% sudo env PATH=/util/ocaml/bin:${PATH} make install

  depends on ocamlgraph
% cd ocamlgraph-1.8.6
% ./configure
% make
% sudo make install

  depends on zarith
% cd zarith-1.4.1
% ./configure
% make
% sudo env PATH=/util/ocaml/bin:${PATH} make install

---

Coq:   http://coq.inria.fr

  depends on lablgtk

% cd coq-8.5
% ./configure -prefix /util/coq-8.5
% make
% 


Why3:   http://why3.lri.fr

---

OPAM might be the way to do this.  Write an OPAM procedure.

Install GTKSourceView.  OPAM relies in GTKSourceView.


% opam repo add coq-released https://coq.inria.fr/opam/released
% opam install coq-of-ocaml


% opam update
% opam install alt-ergo altgr-ergo satML-plugin

% opam install why3 altergo
% why3 --version

References

1. https://wiki.gnome.org/Projects/GtkSourceView
2. https://github.com/ocaml/camlp4/tree/4.02
3. http://ocamlgraph.lri.fr/
4. https://forge.ocamlcore.org/projects/zarith
5. http://wwwfun.kurims.kyoto-u.ac.jp/soft/lsl/lablgtk.html
6. https://github.com/coq/coq/tree/v8.4

References

1. https://opam.ocaml.org/
2. https://github.com/clarus/coq-of-ocaml