We've completed a theory and want to submit it to the AFP. However, during submission, an error of
*** Outer syntax error (line 9 of "~/thy/Polygonal_Number_Theorem/Polygonal_Number_Theorem_Lemmas.thy"): document source expected,
*** but bad input ‹ (line 9 of "~/thy/Polygonal_Number_Theorem/Polygonal_Number_Theorem_Lemmas.thy") was found
As the error suggests, line 9 of the document is
section ‹ Technical Lemmas ›
Does anyone know what is happening here?
Wild guess: do you have a UTF-8
‹ instead of a raw
\<open>? (you need to look at the raw file, not the version interpreted by Isabelle/jEdit)
Hi Chris, my guess is that it is due to some errors when generating LaTex/pdfs (rather than incorrect proofs). To quickly debug such errors, it might be easier to do your local build instead of going through the AFP submission process. Local build can be done via command like
isabelle2022 build -o document=pdf -o document_output="output" -c -D Polygonal_Number_Theorem, where
isabelle2022 should be an Isabelle binary -- on my Mac it is
Thank you Wenda! It all works now! @Wenda Li
Thank you @Mathias Fleury , indeed, GitHub changed our codes a bit. It all works now!
Last updated: Dec 07 2023 at 20:16 UTC