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!

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 `/Applications/Isabelle2022.app/bin/Isabelle`

.

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: Feb 27 2024 at 08:17 UTC