From: Viorel Preoteasa <viorel.preoteasa@abo.fi>
I am trying to build the document for a number of theories in Windows.
I am using the the IsaMakeFile:
default: marking
images:
test: marking
all: images test
SRC = $(ISABELLE_HOME)/src
OUT = $(ISABELLE_OUTPUT)
LOG = $(OUT)/log
USEDIR = $(ISABELLE_TOOL) usedir -v true -i true -d pdf ## -D generated
marking: $(LOG)/HOL-marking.gz
$(LOG)/HOL-marking.gz: ROOT.ML document/root.tex *.thy
@$(USEDIR) HOL .
clean:
@rm -f $(LOG)/HOL-marking.gz
The command isabelle make exits with the following output:
...
*** Output written on root.pdf (46 pages, 177729 bytes).
*** Transcript written on root.log.
*** Document preparation failure in directory
'/cygdrive/c/users/viorel/.isabelle/browser_info/HOL/./document'
*** Failed to build document
"/cygdrive/c/users/viorel/.isabelle/browser_info/HOL/./document.pdf"
make: ***
[/cygdrive/c/users/viorel/.isabelle/heaps/Isabelle2009-1/polyml-5.3.0_x86-cygwin/log/HOL-marking.gz]
Error 1
The file root.pdf seems to be OK, as well as the generated html files.
Best regards,
Viorel Preoteasa
From: Makarius <makarius@sketis.net>
I would say there is some latex error hidden in the "..." above. It
should something like "see also .../log/...", where you can inspect the
complete log file, using the less shell command, for example.
Makarius
Last updated: Nov 21 2024 at 12:39 UTC