I am having trouble to run the codes about Logics and Reasoning in: https://www.cl.cam.ac.uk/~jrh13/atp/
For instance, in the most recent versions, it seems that the new versions do not recognise the Num library. I tried with different online compilers, but all of them fail at some point. Then, the only way is to install the exact version in which the code was written: 3.09.3
So, the question is: how can I install that version? Can I downgrade my Opam? Or would you recommend another option. I use a Mac.
I tried opam switch create 3.09.3 and these problem were reported:
The following actions failed
│ λ build ocaml-base-compiler 3.09.3
└─
┌─ The following changes have been performed (the rest was aborted)
│ ∗ install base-bigarray base
│ ∗ install base-threads base
│ ∗ install base-unix base
You're installing everything correctly and there is no need to downgrade opam. You didn't actually show what was the problem. The error message shows that something has finally failed, but the actual error message was above. There was also a message that contains paths to error logs. I tried to install 3.09.3 on mine machine using opam switch create 3.09.3 and it went without any issues,
$ opam switch create 3.09.3
<><> Gathering sources ><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
[ocaml-base-compiler.3.09.3] downloaded from cache at https://opam.ocaml.org/cache
<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
∗ installed base-bigarray.base
∗ installed base-threads.base
∗ installed base-unix.base
∗ installed ocaml-base-compiler.3.09.3
∗ installed ocaml-config.1
∗ installed ocaml.3.09.3
Done.
So it could be that there were some issues local to your system, like you run out of space, for example.
With that said, you can still try to run these examples in the modern version of OCaml. To enable nums in the modern versions of OCaml, you need to install the package (which is no longer distributed along the OCaml compiler but is still available in opam),
opam install num
Then, you can load num in a toplevel (the ocaml interpreter), using the following
#use "topfind";;
#require "num-top";
The num-top library will load the nums library and even install toplevel printers to make your interacting with arbitrary precision numbers more comfortable. Those two lines should go instead of the #load "nums.cma";; line in the init.ml file.