search

MathHubInfo / Frontend

A new MathHub Narration Frontend written in React.
GNU Affero General Public License v3.0
2 stars 0 forks source link

make the OAF libraries browsable in practice #68

Open kohlhase opened 8 years ago

kohlhase commented 8 years ago

We should add all oaf libraries to MathHub. The ones that should be ready to do are

tkw1536 commented 3 years ago

We should add all of these to MathHub. Not sure why we haven't enabled them yet.

Jazzpirate commented 3 years ago

TPS doesn't exist, but you're missing (at least?) Coq, PVS and IMPS, I guess...?

kohlhase commented 3 years ago

TPS used to exist, it has to be somewhere.

Jazzpirate commented 3 years ago

I'm pretty sure it doesn't ;) I remember you once giving me the OMDoc and wanting me to write an importer (that was years ago in Bremen), at which I failed because I was a) busy with other things and b) incapable of understanding where the URIs point to, and hence, resolving them to anything meaningful.

Unless someone else has done it in the meantime, I'm pretty sure that is still the state of TPS.

kohlhase commented 3 years ago

We seem to have a different notion of existence, whereas for you that means "readable by MMT" I am less discerning.

Jazzpirate commented 3 years ago

well, if it's not readable by MMT, I'm pretty sure MathHub can't do anything with it...?

kohlhase commented 3 years ago

In any case, we need at least one more library to have a credible MWS search paper.

Jazzpirate commented 3 years ago

What about the others I mentioned? PVS, Coq, IMPS... PVS might be a good target since that one should "work" and not be as overwhelmingly large as Coq, and IMPS... I don't know, we'd have to ask Jonas

kohlhase commented 3 years ago

Yes, PVS would be a very good target, especially, since we know that the MMT is OK.

Jazzpirate commented 3 years ago

(or at least should be)

tkw1536 commented 3 years ago

I'll try and load PVS today then and see what happens.