search

dominique-unruh / qrhl-tool

Proof assistant for qRHL
https://dominique-unruh.github.io/qrhl-tool/
MIT License
18 stars 3 forks source link

QRHL 0.5 is not working on my Ubuntu VPS #14

Closed hien-chu closed 4 years ago

hien-chu commented 4 years ago

I hope you can consider the following error that occurs while I try to build Isabelle on VPS

Thank you so much in advanced!

dominique-unruh commented 4 years ago

Does bin/qrhl examples/example.qrhl work?

If not, try running bin/qrhl -Dorg.slf4j.simpleLogger.defaultLogLevel=debug examples/example.qrhl to get some debug information.

Also, maybe it would be easier to read to add command output as text instead of as a picture.

hien-chu commented 4 years ago

Here is the debug text. I'm sorry that I'm still new to github :)

root@vultr:~/QRHL# bin/qrhl -Dorg.slf4j.simpleLogger.defaultLogLevel=debug examples/example.qrhl [main] DEBUG hashedcomputation.DefaultContext - Checking: ec6919b54d58fc2fb613862b65b6a48b82e1969b [main] DEBUG hashedcomputation.DefaultContext - Computing: ec6919b54d58fc2fb613862b65b6a48b82e1969b No current goal. Loading Isabelle. [main] DEBUG qrhl.isabelle.DistributionDirectory - Distribution directory = /root/QRHL [main] DEBUG info.hupel.isabelle.setup.Resolver.Classpath - Trying to resolve PIDE jar from classpath [main] DEBUG info.hupel.isabelle.setup.Resolver.Classpath - Dumping PIDE jar to /tmp/pide15119220352241165100.jar ... [scala-execution-context-global-11] DEBUG info.hupel.isabelle.api.Environment - Creating environment with classpath /tmp/pide15119220352241165100.jar ... [scala-execution-context-global-11] DEBUG info.hupel.isabelle.api.Environment - Instantiating environment at /root/QRHL/Isabelle2019-RC4 (with user storage /root/QRHL/isabelle-temp/user/Isabelle2019-RC4) ... [scala-execution-context-global-11] DEBUG info.hupel.isabelle.api.Environment - Initializing components ... [scala-execution-context-global-11] DEBUG info.hupel.isabelle.api.Environment - Adding component /root/QRHL/isabelle-afp ... [scala-execution-context-global-11] DEBUG info.hupel.isabelle.api.Environment - Adding component /root/QRHL/isabelle-thys ... *** Building Isabelle (may take a while, especially the first time, e.g., 20-60min)... [main] DEBUG info.hupel.isabelle.api.Environment - Building session QRHL ... [main] DEBUG info.hupel.isabelle.api.Environment - QRHL: Session Pure/Pure [main] DEBUG info.hupel.isabelle.api.Environment - QRHL: Session FOL/FOL [main] DEBUG info.hupel.isabelle.api.Environment - QRHL: Session HOL/HOL (main) [main] DEBUG info.hupel.isabelle.api.Environment - QRHL: Session AFP/Cauchy (AFP) [main] DEBUG info.hupel.isabelle.api.Environment - QRHL: Session AFP/Sqrt_Babylonian (AFP) [main] DEBUG info.hupel.isabelle.api.Environment - QRHL: Session HOL/HOL-Cardinals (timing) [main] DEBUG info.hupel.isabelle.api.Environment - QRHL: Session HOL/HOL-Eisbach [main] DEBUG info.hupel.isabelle.api.Environment - QRHL: Session HOL/HOL-Library (main timing) [main] DEBUG info.hupel.isabelle.api.Environment - QRHL: Session AFP/Binomial-Heaps (AFP) [main] DEBUG info.hupel.isabelle.api.Environment - QRHL: Session AFP/Efficient-Mergesort (AFP) [main] DEBUG info.hupel.isabelle.api.Environment - QRHL: Session AFP/Finger-Trees (AFP) [main] DEBUG info.hupel.isabelle.api.Environment - QRHL: Session HOL/HOL-Computational_Algebra (main timing) [main] DEBUG info.hupel.isabelle.api.Environment - QRHL: Session HOL/HOL-Algebra (main timing) [main] DEBUG info.hupel.isabelle.api.Environment - QRHL: Session AFP/VectorSpace (AFP) [main] DEBUG info.hupel.isabelle.api.Environment - QRHL: Session HOL/HOL-Analysis (main timing) [main] DEBUG info.hupel.isabelle.api.Environment - QRHL: Session AFP/Coinductive (AFP) [main] DEBUG info.hupel.isabelle.api.Environment - QRHL: Session HOL/HOL-Probability (main timing) [main] DEBUG info.hupel.isabelle.api.Environment - QRHL: Session AFP/Monad_Normalisation (AFP) [main] DEBUG info.hupel.isabelle.api.Environment - QRHL: Session AFP/Monomorphic_Monad (AFP) [main] DEBUG info.hupel.isabelle.api.Environment - QRHL: Session AFP/Rank_Nullity_Theorem (AFP) [main] DEBUG info.hupel.isabelle.api.Environment - QRHL: Session AFP/Gauss_Jordan (AFP) [main] DEBUG info.hupel.isabelle.api.Environment - QRHL: Session HOL/HOL-Nonstandard_Analysis (timing) [main] DEBUG info.hupel.isabelle.api.Environment - QRHL: Session HOL/HOL-Number_Theory (main timing) [main] DEBUG info.hupel.isabelle.api.Environment - QRHL: Session HOL/HOL-ex (timing) [main] DEBUG info.hupel.isabelle.api.Environment - QRHL: Session AFP/Automatic_Refinement (AFP) [main] DEBUG info.hupel.isabelle.api.Environment - QRHL: Session AFP/Polynomial_Interpolation (AFP) [main] DEBUG info.hupel.isabelle.api.Environment - QRHL: Session HOL/HOL-Imperative_HOL (timing) [main] DEBUG info.hupel.isabelle.api.Environment - QRHL: Session HOL/HOL-ZF [main] DEBUG info.hupel.isabelle.api.Environment - QRHL: Session AFP/Landau_Symbols (AFP) [main] DEBUG info.hupel.isabelle.api.Environment - QRHL: Session AFP/Program-Conflict-Analysis (AFP) [main] DEBUG info.hupel.isabelle.api.Environment - QRHL: Session AFP/Regular-Sets (AFP) [main] DEBUG info.hupel.isabelle.api.Environment - QRHL: Session AFP/Abstract-Rewriting (AFP) [main] DEBUG info.hupel.isabelle.api.Environment - QRHL: Session AFP/Matrix (AFP) [main] DEBUG info.hupel.isabelle.api.Environment - QRHL: Session AFP/Trie (AFP) [main] DEBUG info.hupel.isabelle.api.Environment - QRHL: Session HOL/HOL-Types_To_Sets [main] DEBUG info.hupel.isabelle.api.Environment - QRHL: Session AFP/Banach_Steinhaus (AFP) [main] DEBUG info.hupel.isabelle.api.Environment - QRHL: Session HOL/HOL-Word (main timing) [main] DEBUG info.hupel.isabelle.api.Environment - QRHL: Session AFP/Native_Word (AFP) [main] DEBUG info.hupel.isabelle.api.Environment - QRHL: Session AFP/Refine_Monadic (AFP) [main] DEBUG info.hupel.isabelle.api.Environment - QRHL: Session AFP/Collections (AFP) [main] DEBUG info.hupel.isabelle.api.Environment - QRHL: Session AFP/Deriving (AFP) [main] DEBUG info.hupel.isabelle.api.Environment - QRHL: Session AFP/CAVA_Base (AFP) [main] DEBUG info.hupel.isabelle.api.Environment - QRHL: Session AFP/CAVA_Automata (AFP) [main] DEBUG info.hupel.isabelle.api.Environment - QRHL: Session AFP/DFS_Framework (AFP) [main] DEBUG info.hupel.isabelle.api.Environment - QRHL: Session AFP/Containers (AFP) [main] DEBUG info.hupel.isabelle.api.Environment - QRHL: Session AFP/Collections_Examples (AFP) [main] DEBUG info.hupel.isabelle.api.Environment - QRHL: Session AFP/Show (AFP) [main] DEBUG info.hupel.isabelle.api.Environment - QRHL: Session AFP/JNF-AFP-Lib (AFP) [main] DEBUG info.hupel.isabelle.api.Environment - QRHL: Session AFP/Real_Impl (AFP) [main] DEBUG info.hupel.isabelle.api.Environment - QRHL: Session AFP/Dijkstra_Shortest_Path (AFP) [main] DEBUG info.hupel.isabelle.api.Environment - QRHL: Session AFP/Separation_Logic_Imperative_HOL (AFP) [main] DEBUG info.hupel.isabelle.api.Environment - QRHL: Session AFP/Sepref_Prereq (AFP) [main] DEBUG info.hupel.isabelle.api.Environment - QRHL: Session Doc/Isar_Ref (doc) [main] DEBUG info.hupel.isabelle.api.Environment - QRHL: Session AFP/List-Index (AFP) [main] DEBUG info.hupel.isabelle.api.Environment - QRHL: Session AFP/Refine_Imperative_HOL (AFP) [main] DEBUG info.hupel.isabelle.api.Environment - QRHL: Session AFP/Sepref_Basic (AFP) [main] DEBUG info.hupel.isabelle.api.Environment - QRHL: Session AFP/Sepref_IICF (AFP) [main] DEBUG info.hupel.isabelle.api.Environment - QRHL: Session AFP/Flow_Networks (AFP) [main] DEBUG info.hupel.isabelle.api.Environment - QRHL: Session AFP/EdmondsKarp_Maxflow (AFP) [main] DEBUG info.hupel.isabelle.api.Environment - QRHL: Session AFP/MFMC_Countable (AFP) [main] DEBUG info.hupel.isabelle.api.Environment - QRHL: Session AFP/Partial_Function_MR (AFP) [main] DEBUG info.hupel.isabelle.api.Environment - QRHL: Session AFP/Polynomial_Factorization (AFP) [main] DEBUG info.hupel.isabelle.api.Environment - QRHL: Session AFP/Jordan_Normal_Form (AFP) [main] DEBUG info.hupel.isabelle.api.Environment - QRHL: Session Unsorted/Bounded_Operators-Prerequisites [main] DEBUG info.hupel.isabelle.api.Environment - QRHL: Session Unsorted/Bounded_Operators [main] DEBUG info.hupel.isabelle.api.Environment - QRHL: Session Unsorted/Tensor_Product [main] DEBUG info.hupel.isabelle.api.Environment - QRHL: Session Unsorted/QRHL-Prerequisites1 [main] DEBUG info.hupel.isabelle.api.Environment - QRHL: Session AFP/Subresultants (AFP) [main] DEBUG info.hupel.isabelle.api.Environment - QRHL: Session AFP/Pre_BZ (AFP) [main] DEBUG info.hupel.isabelle.api.Environment - QRHL: Session AFP/Probabilistic_While (AFP) [main] DEBUG info.hupel.isabelle.api.Environment - QRHL: Session HOL/HOL-Proofs (timing) [main] DEBUG info.hupel.isabelle.api.Environment - QRHL: Session HOL/HOL-Proofs-Lambda (timing) [main] DEBUG info.hupel.isabelle.api.Environment - QRHL: Session AFP/Applicative_Lifting (AFP) [main] DEBUG info.hupel.isabelle.api.Environment - QRHL: Session AFP/CryptHOL (AFP) [main] DEBUG info.hupel.isabelle.api.Environment - QRHL: Session Unsorted/QRHL-Prerequisites2 [main] DEBUG info.hupel.isabelle.api.Environment - QRHL: Session Unsorted/Multi_Isabelle [main] DEBUG info.hupel.isabelle.api.Environment - QRHL: Session Unsorted/Classy [main] DEBUG info.hupel.isabelle.api.Environment - QRHL: Session Tools/Spec_Check [main] DEBUG info.hupel.isabelle.api.Environment - QRHL: Session Unsorted/Protocol [main] DEBUG info.hupel.isabelle.api.Environment - QRHL: Session Unsorted/HOL-Protocol [main] DEBUG info.hupel.isabelle.api.Environment - QRHL: Session Unsorted/QRHL-Prerequisites [main] DEBUG info.hupel.isabelle.api.Environment - QRHL: Session Unsorted/QRHL-Bounded_Operators [main] DEBUG info.hupel.isabelle.api.Environment - QRHL: Session Unsorted/QRHL-Tensor_Product [main] DEBUG info.hupel.isabelle.api.Environment - QRHL: Session Unsorted/QRHL [main] DEBUG info.hupel.isabelle.api.Environment - QRHL: Building Pure ... [main] DEBUG info.hupel.isabelle.api.Environment - QRHL: Pure FAILED [main] DEBUG info.hupel.isabelle.api.Environment - QRHL: (see also /root/QRHL/isabelle-temp/user/Isabelle2019-RC4/.isabelle/Isabelle2019-RC4/heaps/polyml-5.8_x86_64_32-linux/log/Pure) val id: string -> T val id_only: string -> T val id_properties_of: T -> Properties.T val is_reported: T -> bool val is_reported_range: T -> bool val line: int -> T val line_file: int -> string -> T val line_file_only: int -> string -> T val line_of: T -> int option val make: Thread_Position.T -> T val markup: T -> Markup.T -> Markup.T val no_range: range val no_range_position: T -> T val none: T val of_properties: Properties.T -> T val offset_of: T -> int option val offset_properties_of: T -> Properties.T val parse_id: T -> int option val properties_of: T -> Properties.T val properties_of_range: range -> Properties.T val put_id: string -> T -> T val range: T T -> range type range = T T val range_of_properties: Properties.T -> range val range_position: range -> T type report = T Markup.T val report: T -> Markup.T -> unit type report_text = report string val report_text: T -> Markup.T -> string -> unit val reported_text: T -> Markup.T -> string -> string val reports: report list -> unit val reports_text: report_text list -> unit val setmp_thread_data: T -> ('a -> 'b) -> 'a -> 'b val start: T val store_reports: report_text list ref -> T list -> ('a -> Markup.T list) -> 'a -> unit val thread_data: unit -> T end structure Position: POSITION val it = (): unit [main] DEBUG info.hupel.isabelle.api.Environment - QRHL: HOL CANCELLED [main] DEBUG info.hupel.isabelle.api.Environment - QRHL: HOL-Analysis CANCELLED [main] DEBUG info.hupel.isabelle.api.Environment - QRHL: Bounded_Operators-Prerequisites CANCELLED [main] DEBUG info.hupel.isabelle.api.Environment - QRHL: QRHL-Prerequisites1 CANCELLED [main] DEBUG info.hupel.isabelle.api.Environment - QRHL: QRHL-Prerequisites2 CANCELLED [main] DEBUG info.hupel.isabelle.api.Environment - QRHL: QRHL-Prerequisites CANCELLED [main] DEBUG info.hupel.isabelle.api.Environment - QRHL: QRHL-Bounded_Operators CANCELLED [main] DEBUG info.hupel.isabelle.api.Environment - QRHL: QRHL-Tensor_Product CANCELLED [main] DEBUG info.hupel.isabelle.api.Environment - QRHL: QRHL CANCELLED [main] DEBUG info.hupel.isabelle.api.Environment - QRHL: Unfinished session(s): Bounded_Operators-Prerequisites, HOL, HOL-Analysis, Pure, QRHL, QRHL-Bounded_Operators, QRHL-Prerequisites, QRHL-Prerequisites1, QRHL-Prerequisites2, QRHL-Tensor_Product [ERROR] examples/example.qrhl:1: Building Isabelle failed

dominique-unruh commented 4 years ago 
[main] DEBUG info.hupel.isabelle.api.Environment - QRHL: (see also /root/QRHL/isabelle-temp/user/Isabelle2019-RC4/.isabelle/Isabelle2019-RC4/heaps/polyml-5.8_x86_64_32-linux/log/Pure)

Can you show the file mentioned here? Probably (hopefully) the error message is in there.

(Large log files can also be attached to a comment as a file by drag & drop.)

hien-chu commented 4 years ago

I guess (not sure) that here is the log file :)

root@vultr:~/QRHL/isabelle-temp/user/Isabelle2019-RC4/.isabelle/Isabelle2019-RC4/heaps/polyml-5.8_x86_64_32-linux/log# bash Pure Pure: line 1: signature: command not found Pure: line 2: sig: command not found Pure: line 3: exception: command not found Pure: line 4: val: command not found Pure: line 6: end: command not found Pure: line 7: signature: command not found Pure: line 8: sig: command not found Pure: line 9: exception: command not found Pure: line 10: exception: command not found Pure: line 11: exception: command not found Pure: line 12: syntax error near unexpected token (' Pure: line 12: val capture: ('a -> 'b) -> 'a -> 'b result'

hphuoctruong commented 4 years ago

Pure.log I think this is the log-file in the comment of hien-chu. I also had the same problem while installing on an Ubuntu VPS.

dominique-unruh commented 4 years ago

There is no error message to be found anywhere... Maybe the VPS runs out of ressources? You could check if Isabelle works at all. In the qrhl-directory run:

isabelle-temp/setups/Isabelle2019/bin/isabelle build -v -b HOL-Analysis

(not 100% sure about the filename) and see what happens. (Afterwards, delete ~/.isabelle since it will waste a lot of space.)

hphuoctruong commented 4 years ago

Thank you very much. It is definitely because of the resource problem! I replaced my old VPS with a stronger one and it worked well! I guess it's also the reason why QRHL did not work when I tried installing in Ubuntu, using VM VirtualBox.

dominique-unruh commented 4 years ago

I'm glad it worked.

Can you let me know what the resource limits where (amount of memory, and – if applicable – runtime limits)? (The commands ulimit -a and free -h might give useful information.)

It would be good to know what the limits are, especially since there seems to be no useful error message when the process gets killed due to resource exhaustion.

hphuoctruong commented 4 years ago

Here are the details. The weak one

Screen Shot 2020-09-21 at 00 00 14

weakVPS.log

The powerful one

Screen Shot 2020-09-21 at 00 10 29

powerfulVPS.log

It seems that there is a big gap between the weak one and the powerful one. I am sorry since I haven't tried any VPSs in the middle.

dominique-unruh commented 4 years ago

Thanks for the info. Indeed, the weak one has 1GB of memory. I don't know how much is needed, but I am very sure that 1GB is not enough. So the process got killed by an out of memory error.