search

UniFormal / MMT

The MMT Language and System
https://uniformal.github.io/
Other
68 stars 22 forks source link

Loading Isabelle on MathHub seems to cause an infinite loop #562

Closed tkw1536 closed 3 years ago

tkw1536 commented 3 years ago

When loading the Isabelle archives on MathHub, this seems to prevent MMT from doing anything.

In particular, the server seems to run into an infinite loop and not do anything anymore. I am not sure if this is a core MMT issue (of scaling) or a MathHub specific issue.
I will investigate this and document the results in this issue.

Jazzpirate commented 3 years ago

Can you explain what you mean by "loading the archives"?

Do you mean reading the relational files or actively retrieving content (e.g. to present it somewhere)?

tkw1536 commented 3 years ago

"loading the archive" means "archive add" followed by trying to get the narrative root document of the archive

Jazzpirate commented 3 years ago

:O That seems.... highly inlikely. Both of those only entail "reading the MANIFEST.MF"...??

(...something that works fine on my system, btw, as does loading the relational info, on both Isabelle-archives, so I'm inclined to think it's more a MathHub-Problem than one with MMT...?)

Jazzpirate commented 3 years ago

oh wait - what do you mean by "getting the narrative root document"? Like, the narrative root is just a DPath in the MANIFEST.MF. There does not need to exist an actual document with that URI... which one is it in your case?

tkw1536 commented 3 years ago

I do mean .geting that DPath. The document is generated dynamically somewhere inside mmt-api, and this works perfectly fine for other archives. It typically only contains references to all .omdoc files in the archive.

Jazzpirate commented 3 years ago

I do mean .geting that DPath. The document is generated dynamically somewhere inside mmt-api, and this works perfectly fine for other archives. It typically only contains references to all .omdoc files in the archive.

Ooooh! I did not know that. In that case it is very possible that MMT doesn't run in an infinite loop, but rather runs for quite a while, and possibly runs into memory-exceptions. The AFP archive is massive, and if generating that document requires loading all archive content, that might be an issue... (or there are content errors with some of the content, of course...) do you have a log file or something? And if so does that log "debug" (i.e. all exceptions and errors with full stack trace)?

tkw1536 commented 3 years ago

Figured out where this came from. This was caused by trying to load statistics for the archive. That tried to recursively load the entire archive.

I've built a workaround that only enables statistics if the "statistics" key in manifest.mf is set to true.