retest this project with the Lean data set

[timabbott]

@robertylewis I just merge a series of commits, inspired by some work the rust-lang folks did in integrating this, that moves a bunch of the configuration settings to live in the zuliprc file. Docs are present in the README.md. Can you test it out and make sure it didn't break anything for Lean?

Also you may want to look at the Rust folks changes: https://github.com/zulip/zulip_archive/commits/rust-remaining to see if any of those you'd like for Lean as well. Here are my notes to them on next steps:

• The "move CSS to separate file" commit we should just rebase to the bottom and merge.
• For sort order, was the previous sort order "by last update"? I think both are potentially useful, so I wouldn't want to unconditionally apply that change. Ideally we'd just include something simple like sortable.js that allows the user to pick, and maybe have a config option for which is the default. So I'd probably tweak the commit to be an option for the default view and merge it, and then we can open an issue for adding JS sorting.
• For the "Reformat" commit, we may need to split it. I suspect some of the styling changes may just be better for everyone. I don't fully understand the "last_updated" change; I think the intent of the previous model was to avoid needing to rewrite all the HTML/markdown when run in incremental mode, and I'm not sure if your restructuring loses that. Maybe it makes sense to open issues/small PRs for each independent change so we can see what the lean folks' original author thinks?

On question I had for you:

• Would it make sense to move the code for pushing this to a GitHub Pages site to a separate script? The Rust folks removed that functionality in their branch I think mostly to declutter things, and I think I agree it'd be cleaner if that was a separate script in this repo that just pushed the archive.

[robertylewis]

I had to change line 181 to site_url / html_root instead of os.path.join since Python complained about joining Path objects. Otherwise it seems to work fine.

The "move CSS to separate file" commit we should just rebase to the bottom and merge.

I'm not sure the script needs to generate CSS at all. We could provide a default (static) css file for the generated pages.

For sort order, was the previous sort order "by last update"?

It was by number of topics, which is a pretty stable measure of "importance." JS sorting sounds great (as long as the default order is customizable).

Would it make sense to move the code for pushing this to a GitHub Pages site to a separate script?

Yeah, we could just add it to the shell script that calls the Python script, no need for it to be in here.

[robertylewis]

think the intent of the previous model was to avoid needing to rewrite all the HTML/markdown when run in incremental mode

This was the intent, but I never actually got around to doing it. Right now, all the HTML/markdown gets regenerated each time, even when you update the archive incrementally. populate_incremental would need to return a list of modified topics for write_markdown to use.

I guess the Rust people aren't using Jekyll, so including the update time with {% %} isn't possible.

[rht]

The remaining 3 commits from rust-remaining branch that have yet to be reconciled with master branch:

1. Put style in style.css (1373f6c)
2. Sort index.html list alphabetically instead of by number of topics (a63a677)
3. Show topic lists more compactly (87918e9)

What should be done for each of the 3?

[timabbott]

Put style in style.css (1373f6c)

This should just be merged unconditionally; it should be simply a better arrangement.

Sort index.html list alphabetically instead of by number of topics (a63a677)

Hmm, this one is a bit more interesting. I think ultimately one will want sort order to be something users can control dynamically with JavaScript. Maybe we should turn this into an issue?

Show topic lists more compactly (87918e9)

Can you post screenshots of the two versions? I think we might just want to figure out which version looks nicer and merge that.

[rht]

Can you post screenshots of the two versions? I think we might just want to figure out which version looks nicer and merge that.

With double newlines: https://leanprover-community.github.io/archive/113488general/index.html
With single newline: https://zulip-archive.rust-lang.org/122651general/index.html

[timabbott]

I think probably the right model is single newlines, and if one wants to do wider spacing between entries, that can be done with CSS. Does that make sense to you @robertylewis?

[robertylewis]

Ah, I didn't think that newline actually had any effect on the HTML output, but apparently it does. It gets compiled to <li><p>...</p></li> in the two-line case, and <li>...</li> with one line. Yes, seems like a reasonable change, the spacing should be handled in the css for list environments.

[timabbott]

OK, I think we've integrated everything from the Rust/Lean branches except for sort order, which I feel like should probably be made available as a JavaScript UI option. @robertylewis @Mark-Simulacrum do you have a chance to test the latest code?

[Mark-Simulacrum]

I will try to resync the rust-lang repository this weekend with this repository.

[Mark-Simulacrum]

% include is emitted into the markdown files which isn't Markdown -- I think we should avoid doing so in the official tool, since it presumes you're using something like Jekyll or a similar markdown renderer which is a superset of markdown.

[rht]

% include is emitted into the markdown files which isn't Markdown -- I think we should avoid doing so in the official tool, since it presumes you're using something like Jekyll or a similar markdown renderer which is a superset of markdown.

Opened #12 to address this.

[timabbott]

Thanks everyone for testing!