I have no idea how to make PVS show on MathHub

[Jazzpirate]

I pushed mh-html and planetary to the PVS archive, pulled it on pine, now it correctly shows pvs.omdoc and pvsxml (here: https://mathhub.info/PVS/Prelude) but clicking on either results in "file not found". No idea how this works...

[kohlhase]

@m-iancu, could you please have a look on this and tell me what you did (and what we did wrong?), that would be very helpful. cc: @tkw1536

[m-iancu]

Looks like Synchronize Nodes fails to find the valid PVS source files. The way it works is by looking in the source folder and find all files for which there is a corresponding log file in the errors folder (i.e. files that were build by the associated importer -- for PVS that is mmt-omdoc in the config). Based on the sources as committed to https://gl.mathhub.info/PVS/Prelude/tree/master, superficially, I see two errors:

• the source folder is called src not source -- i.e. MathHub finds 0 source files
• the errors folder is not committed, so if MathHub were to find a source files foo it would see there is no corresponding errors/mmt-omdoc/foo.log file and assume its not a real source file just a utility/documentation file -- and therefore ignore it.

Fixing these two issues then running sync nodes from the admin page should work (hopefully)