Re: [Hol-info] Installation Problem of HOL-Light

Hi Elif, On 24/06/2020 18:19, elif deniz wrote: Hi Petros, Thank you for your response. Yes, it is warning and seems like running. But, when I want to load "Multivariate/realanalysis.ml " or "Multivariate/cauchy.ml " theories; after loading almost 4

Re: [Hol-info] Installation Problem of HOL-Light

Hi Petros, Thank you for your response. Yes, it is warning and seems like running. But, when I want to load "Multivariate/realanalysis.ml" or "Multivariate/ cauchy.ml" theories; after loading almost 45 minutes, system killed and I couldn't load these theories. So, I thought maybe it is not proper

Re: [Hol-info] Installation Problem of HOL-Light

Dear all, Some time ago (in the times of Debian Stretch :-)) I made a Dockerfile for HOL Light, see the attachment. The commands I used for building the image and running it are: docker build -t hol-light . docker run -i -v /home/freek:/home/freek --name hol-light hol-light You need to run

Re: [Hol-info] Installation Problem of HOL-Light

Hi Elif, I am not sure what went wrong with your first attempt. The chunk you pasted contains no errors, only warnings. The other errors you are getting are errors with installing OCaml. It is trying to install it globally, but you are not giving it permission to do that. You can either (a

[Hol-info] Installation Problem of HOL-Light

Dear all, I'm trying to install HOL-Light on Ubuntu 14.04 and following the instruction on Github website. When I do #use "hol.ml" on ocaml interface, I'm facing the following errors: File "/home/elif/hol-light/impconv.ml" , line 315, characters 8-174: Warning 8: this pattern-matching is not exha