Stream: Beginner Questions

Topic: Failed to submit an AFP entry

view this post on Zulip 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!

view this post on Zulip 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)

view this post on Zulip 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/

view this post on Zulip Chris_Y (Aug 10 2023 at 17:12):

Thank you Wenda! It all works now! @Wenda Li

view this post on Zulip 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: Dec 07 2023 at 20:16 UTC