Zulip Chat Archive

Stream: general

Topic: leanprover community website asks to push large files

Shreyas Srinivas (Oct 14 2023 at 15:12):

As the title says, I am not able to push very tiny changes I made to the website pages to github (my own fork from which a PR will follow).

Shreyas Srinivas (Oct 14 2023 at 15:13):

The error is 

remote: error: Trace: 52c2bf60a313d02830d9912272d066f3f2cd6c798c17ba1cafb5ea725739330e
remote: error: See https://gh.io/lfs for more information.
remote: error: File data/header-data.json is 458.28 MB; this exceeds GitHub's file size limit of 100.00 MB
remote: error: GH001: Large files detected. You may want to try Git Large File Storage - https://git-lfs.github.com.
To github.com:Shreyas4991/leanprover-community.github.io.git
 ! [remote rejected]     lean4 -> lean4 (pre-receive hook declined)
error: failed to push some refs to 'github.com:Shreyas4991/leanprover-community.github.io.git'

Shreyas Srinivas (Oct 14 2023 at 15:13):

What's the standard work around? git lfs?

Shreyas Srinivas (Oct 14 2023 at 15:14):

should this header.json file just be ignored?

Shreyas Srinivas (Oct 14 2023 at 15:15):

I didn't touch this file but it seems to be there in the diffs (at least after make_site.py was called)

Eric Wieser (Oct 14 2023 at 16:18):

I think that file should be ignored

Utensil Song (Oct 14 2023 at 16:20):

The better approach nowadays is to move from pushing to branch gh-pages (or repo *.github.io) to Publishing with a custom GitHub Actions workflow (e.g. these configs also note the permissions above).

Eric Wieser (Oct 14 2023 at 16:22):

That doesn't work well for us because the webpage contains the union of two branches (lean3 + Lean4)

Utensil Song (Oct 14 2023 at 16:27):

Could Lean 4 workflow just pull things from Lean 3 built artifacts, merge locally and upload the artifacts altogether?

Eric Wieser (Oct 14 2023 at 16:29):

Yes, but I think fetching the artifacts is tricky

Eric Wieser (Oct 14 2023 at 16:29):

At any rate, CI already works fine here; @Shreyas Srinivas is presumably trying to run things manually instead of using the existing CI setup.

Utensil Song (Oct 14 2023 at 16:31):

Is data/header-data.json meant to be consumed by browser, or should it simply be ignored in .gitignore?

Shreyas Srinivas (Oct 14 2023 at 16:32):

I am not sure I can commit directly

Eric Wieser (Oct 14 2023 at 16:46):

Shreyas Srinivas said:

I am not sure I can commit directly

Make a fork and push to your fork

Eric Wieser (Oct 14 2023 at 16:47):

Utensil Song said:

Is data/header-data.json meant to be consumed by browser, or should it simply be ignored in .gitignore?

It's a temporary file used in the build

Shreyas Srinivas (Oct 14 2023 at 16:47):

Eric Wieser said:

Shreyas Srinivas said:

I am not sure I can commit directly

Make a fork and push to your fork

Whence the problem. I don't have any CI setup.

Eric Wieser (Oct 14 2023 at 16:47):

Your fork should have the ci setup inside it

Eric Wieser (Oct 14 2023 at 16:47):

It's in the .github folder

Shreyas Srinivas (Oct 14 2023 at 16:47):

okay. I'll check and get back

Eric Wieser (Oct 14 2023 at 16:48):

You might need to click a button saying "yes run CI" somewhere obvious

Utensil Song (Oct 14 2023 at 16:54):

I checked the repo, nothing has been committed to github yet, it's stuck before CI stuff. @Shreyas Srinivas you can add data/header-data.json to your .gitignore and try commit again. It shouldn't be committed as it's just a temporary file retrieved here and not used afterwards.

Utensil Song (Oct 14 2023 at 16:56):

This is the yes button in case there's any confusion:

image.png

Shreyas Srinivas (Oct 14 2023 at 16:58):

Yeah this is definitely a build artifact. I can't see this file in the main repo. I have now pushed two commits and will be opening the PR.

Shreyas Srinivas (Oct 14 2023 at 17:04):

Here it is

Shreyas Srinivas (Oct 14 2023 at 17:06):

For now I have added:

  1. A new troubleshooting page with basic text.
  2. A menu entry.
  3. Added the build artifact data/header-data.json to .gitignore.

Shreyas Srinivas (Oct 14 2023 at 17:07):

Ideally before the PR is accepted, I would like to add a few common problems and solutions, including things people faced at LfCTM
and in lectures. Problems w.r.t installation, firewalls, network connections etc.

Shreyas Srinivas (Oct 14 2023 at 17:11):

I enabled the actions on my repo, essentially what I get is "there are no workflow runs yet"

Utensil Song (Oct 14 2023 at 17:13):

Github actions workflow runs require a trigger, such as a push after you enable it, or scheduled runs, or manual trigger.

Shreyas Srinivas (Oct 14 2023 at 17:18):

Okay. I can test this with my next commit where I add some footguns that have already been mentioned here. I will need to collect some details though.

Shreyas Srinivas (Oct 14 2023 at 17:30):

@Eric Wieser : Can I list the windows issue to start the page off?

Last updated: Dec 20 2023 at 11:08 UTC