What semantics do you use for your HOL library? I scanned around but documentation on that page is a bit sparse. The github repo goes to a random user's page, and all I could find there was this unrelated repo: https://github.com/digama0/HOL

Yeah, that github URL should be fixed. The HOL database is here https://github.com/metamath/set.mm/blob/develop/hol.mm