Chris_Y (Aug 10 2023 at 14:32): Chris_Y (Aug 10 2023 at 14:32):Hi everyone,
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
kept appearing.
As the error suggests, line 9 of the document is
section ‹ Technical Lemmas ›
Does anyone know what is happening here?
Many thanks!
Mathias Fleury (Aug 10 2023 at 15:41):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)
Wenda Li (Aug 10 2023 at 15:45):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 /Applications/Isabelle2022.app/bin/Isabelle.
Chris_Y (Aug 10 2023 at 17:12):Thank you Wenda! It all works now! @Wenda Li
Chris_Y (Aug 10 2023 at 17:13):Thank you @Mathias Fleury , indeed, GitHub changed our codes a bit. It all works now!
Last updated: Apr 27 2024 at 20:14 UTC