Email Gateway (Aug 18 2022 at 09:58): Email Gateway (Aug 18 2022 at 09:58):From: clefort <ipub@charter.net>
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
Email Gateway (Aug 18 2022 at 09:59):From: Michael Nedzelsky <MichaelNedzelsky@yandex.ru>
It seems you need invoke build script from Isabelle distribution in order to
compile objects logics. See INSTALL (section "Compiling logics").
Regards,
Michael Nedzelsky
Email Gateway (Aug 18 2022 at 09:59):From: Primrose.Mbanefo@Infineon.com
Hi,
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
Strange... I just looked at the precompiled HOL logic for ppc-darwin and
it does also have an "ISABELLE_HOME/heaps/polyml_ppc-darwin/HOL" entry.
Maybe something went wrong while you were untarring the files? Maybe you
should try untarring it again. You can always build it yourself as
suggested.
and I believe it is an HOL heap you are looking for, not an
executable....
Primrose
Last updated: May 03 2024 at 08:18 UTC