Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] building the document fails on Windows


view this post on Zulip Email Gateway (Aug 18 2022 at 15:15):

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:

targets

default: marking
images:
test: marking

all: images test

global settings

SRC = $(ISABELLE_HOME)/src
OUT = $(ISABELLE_OUTPUT)
LOG = $(OUT)/log

USEDIR = $(ISABELLE_TOOL) usedir -v true -i true -d pdf ## -D generated

marking

marking: $(LOG)/HOL-marking.gz

$(LOG)/HOL-marking.gz: ROOT.ML document/root.tex *.thy
@$(USEDIR) HOL .

clean

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

view this post on Zulip Email Gateway (Aug 18 2022 at 15:22):

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: Apr 25 2024 at 20:15 UTC