Various issues with installing a local copy of the site

[Luke Murphy]

I'm working on a data science project about how often each axiom is used in set.mm and iset.mm, so I decided to install a local copy of the site so I could scrape the copy without disrupting the live site, but I've faced three distinct issues in trying to follow the home page's instructions:


1. I can't run install.sh in metamathsite.zip because there is no install.sh in there, so it naturally throws this error:

./install.sh : The term './install.sh' is not recognized as the name of a cmdlet, function, script file, or operable
program. Check the spelling of the name, or if a path was included, verify that the path is correct and try again.
At line:1 char:1
+ ./install.sh
+ ~~~~~~~~~~~~
    + CategoryInfo          : ObjectNotFound: (./install.sh:String) [], CommandNotFoundException
    + FullyQualifiedErrorId : CommandNotFoundException

Also, the zip is actually named "metamath-website-seed-main.zip". Is the link pointing to the wrong zip?


2. rsync fails and throws this error:

$ rsync -vrltS -z --delete --delete-after rsync://rsync.metamath.org/metamath .
rsync: [Receiver] failed to connect to rsync.metamath.org (98.118.4.152): Connection timed out (116)
rsync error: error in socket IO (code 10) at clientserver.c(139) [Receiver=3.3.0]

I don't know how rsync works, so this one might just be on my end.


3. Mercifully, wget does work, but it turns out there are two pairs of theorems that have identical names up to capitalization ("elOLD" and "elold"; "fmptdf" and "fmptdF"), and when downloading their pages, the latter of each pair gets overwritten by the former. I can manually redownload the missing pages, but we should probably forbid such name collisions going forward.

[Eric Schmidt]

1. install.sh was removed in commit 336986ab030417b6a0eefe224f7289f68e72056a. The commit message points to the metamath-website-scripts repo. I suspect that old/install.sh is what would give you greatest chance at success, though that script has been apparently been replaced with build-system.sh and build-website.sh. There might be other missing files. In any case, those directions are obviously quite obsolete. I have created an issue to track this: https://github.com/metamath/metamath-website-seed/issues/36.

2. Don't know about the rsync issue. Perhaps David Wheeler will be able to help.

3. We can easily fix the capitalization issue for now. Preventing future collisions will take more work. I might look into this later.

[Steven Nguyen]

A much easier way to do this is to use metamath-knife. For example, here is the (top of the) axiom graph from two years ago:

 (specifically, https://github.com/metamath/set.mm/pull/4477 )

--
You received this message because you are subscribed to the Google Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email to metamath+u...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/metamath/dd34655a-b9c8-43d3-8597-0f2701da22f9n%40googlegroups.com.

[Luke Murphy]

...Ah. Well, at least I learned how to use Beautiful Soup and pandas.