Is it possible to have an AFP entry with documentation that uses BibLatex as opposed to Bibtex?

Question

I have submitted an entry to the Archive of Formal Proofs (AFP). In the documents folder, I have a root.tex and a root.bib that work with BibLatex. The automated system seems to be trying to use Bibtex to process the bibliography. Is it just not allowed to use BibLatex? Or should I just run biber on my own and provide all the auxiliary files (like root.bbl, etc.). I mean, I have no problem just submitting the root.pdf, but they seem to want source files only.

Again, StackOverflow wants me to did, what I expected to happen, and what resulted. Well, I submitted the AFP entry files. I expected the automated system to build root.pdf, but the automated system didn't even read its own messages, which included the warning:

Package biblatex Warning: Please (re)run Biber on the file:
(biblatex)                root
(biblatex)                and rerun LaTeX afterwards.
)

Answer 1

The AFP submission server runs almost exactly the same code as the Isabelle build system, which makes a few assumptions on how a session is supposed to be structured. As far as I know, it runs a certain sequence of LaTeX-related commands, with no way to change them.

More importantly, the implicit assumption is that users would start out with an Isabelle-generated document file, and then fill that with content. Part of this is described in the Isabelle system manual.

Section 3.2 describes how to generate such a document file (together with everything else needed for a session, such as the ROOT file):

isabelle mkroot My_Session_Directory

To ensure that the current document files that you may already have work according to Isabelle's expectations, you can invoke the build process locally as follows (Section 2.3 in the system manual):

isabelle build -bv -P: -D My_Session_Directory

If that works, it should also work on the AFP submission server.