[isabelle] INstalling Isabelle / sudo and permissions



Thanks to both Primrose and Teme

There isn't any reason I shouldn't have permission on my own machine. Here is the transcript form terminal:

FIRST, permissions:

24-182-155-183:~/Isabelle/Isabelle/ISABELLE_HOME clintonlefort$ sudo ./bin/isatool

Usage: isatool TOOL [ARGS ...]

  Start Isabelle utility program TOOL with ARGS. Pass "-?" to TOOL
  for more specific help.

  Available tools are:
    browser - Isabelle graph browser
convert - convert legacy tactic scripts to Isabelle/Isar tactic emulation
    dimacs2hol - convert DIMACS CNF files into Isabelle/HOL theories
    display - display document (in DVI or PDF format)
    doc - view Isabelle documentation
    document - prepare theory session document
    expandshort - expand shorthand goal commands
    findlogics - collect heap names from ISABELLE_PATH
fixcpure - adapt theories and ML files to new CPure/Pure arrangement
    fixgreek - fix problems with greek and other foreign letters
fixheaders - turn Isar theory headers into imports-uses-begin format
    fixsome - fix theorem names related to SOME (Eps) in HOL
    getenv - get values from Isabelle settings environment
    install - install standalone Isabelle executables
    latex - run LaTeX (and related tools)
    logo - create an instance of the Isabelle logo
    make - Isabelle make utility
    makeall - apply make utility to all logics
    mkdir - prepare logic session directory
    print - print document
    unsymbolize - remove unreadable symbol names from sources
    usedir - build object-logic or run examples
    version - display Isabelle version

SECONDLY as Primrose suggests:

24-182-155-183:~/Isabelle/Isabelle/ISABELLE_HOME clintonlefort$ ./bin/ isatool install -p clintonlefort/bin referring to distribution at /Users/clintonlefort/Isabelle/Isabelle/ ISABELLE_HOME
installing clintonlefort/bin/isatool
installing clintonlefort/bin/isabelle-process
installing clintonlefort/bin/isabelle-interface
installing clintonlefort/bin/Isabelle
installing clintonlefort/bin/isabelle


Then

24-182-155-183:~/Isabelle/Isabelle/ISABELLE_HOME clintonlefort$ ./ clintonlefort/bin/isabelle
Unknown logic "HOL" -- no heap file found in:
  /Users/clintonlefort/isabelle/heaps/polyml_ppc-darwin
/Users/clintonlefort/Isabelle/Isabelle/ISABELLE_HOME/heaps/ polyml_ppc-darwin
24-182-155-183:~/Isabelle/Isabelle/ISABELLE_HOME clintonlefort$


Any insights?

Presently HOL executable is in :
ISABELLE_HOME/heaps/polyml_ppc-darwin/log/HOL where PURE is also
and I am calling Isabelle from  within ISABELLE_HOME dir

still I get this message at terminal

24-182-155-183:~/Isabelle/Isabelle/ISABELLE_HOME clintonlefort$ ./ clintonlefort/bin/isabelle
Unknown logic "HOL" -- no heap file found in:
  /Users/clintonlefort/isabelle/heaps/polyml_ppc-darwin
/Users/clintonlefort/Isabelle/Isabelle/ISABELLE_HOME/heaps/ polyml_ppc-darwin


What can I do?

CL





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.