move images to images/ and update links #3515
Conversation
There was a problem hiding this comment.
I'm fine with this change although it does come with a bit of a disclaimer in that metamath/metamath-website-seed#14 and metamath/metamath-website-scripts#2 may prevent the live site from updating.
Therefore, merging this one will hasten those two ? ;) |
|
I fully support reorganizing the set.mm folder as I found it chaotic and confusing the first times I browsed through it. In #1887 there is a extensive debate, but in the end I think I like the proposal from Mario. I particularly appreciate the concept of creating a separate folder for each .mm database and their own associated files (such as the discouraged files). I'm also persuaded by the suggestion of renaming this repo into I'm aware that reorganizing and renaming are not risk-free, but the thing is I didn't find the research to be intuitive when I first discovered metamath. One of the first things a new user asks is: "Where are all the theorems?". For me the answer didn't come in the form of "Oh that's where they are", but rather in the form of "Set.mm? What's set.mm? Mh, it looks like there is math stuff here, so maybe I'm going in the right direction". In general I felt I was discovering the relevant places "on my own" and I didn't feel guided by metamath to go to the core files. In any case my preference is not too strong, so I'm open to variations. I already appreciate the beginning of the transition from this PR. |
We can always hope but there isn't really any guarantee that one would cause the other - a read through metamath/metamath-website-scripts#2 perhaps makes this clear. |
|
While I am of course in support of this general direction, as my stance on #1887 should make clear, the changes to HTML files in this PR worry me. Is this directory change being replicated on the metamath site? That is, will https://us.metamath.org/mpeuni/_relexample.svg be a 404 after this change? If yes, it might be a bit awkward that some but not all images are in the images directory. If no, the HTML files should not be modified (and we have to make a choice between making the HTML files work in situ in the github repo, or making them work on the website). And in either case, we need to modify the website script because it's not expecting the image files to be at this new location. Put another way, we shouldn't merge this PR without a matching PR to metamath-website-scripts repo. |
jkingdon
dismissed
their stale review
This change will not work with current build scripts
|
I just got back from back-to-back work meetings (DC, Spain). I haven't had a chance to review this yet, but clearly we want to ensure that the results work :-). |
| `scripts/rewrap set.mm` to make sure your pull request passes this check. | ||
|
|
||
| Locally you will need to run `scripts/rewrap set.mm` to avoid failing this | ||
| check. |
There was a problem hiding this comment.
"avoid failing" --> "make sure [it] passes": avoid double negatives
There was a problem hiding this comment.
I don't see any response to
Is this directory change being replicated on the metamath site? That is, will https://us.metamath.org/mpeuni/_relexample.svg be a 404 after this change? If yes, it might be a bit awkward that some but not all images are in the images directory. If no, the HTML files should not be modified (and we have to make a choice between making the HTML files work in situ in the github repo, or making them work on the website). And in either case, we need to modify the website script because it's not expecting the image files to be at this new location.
nor could I see based on looking through https://github.com/metamath/metamath-website-scripts/tree/main how the svg files get copied to the website (the test for whether it worked is whether they are visible in the table at https://us.metamath.org/mpeuni/mmfrege.html ).
The changes to CONTRIBUTING.md look good to me, perhaps that can productively be separated into a different pull request than the creation of an images directory.
I had the same question recently... the answer is that they aren't - the SVGs served on the website are actually https://github.com/metamath/metamath-website-seed/blob/main/mpegif/_frege_A.svg et al (and don't let the |
|
So, should I remove all these svg's in this repo ? But then, what URLs should I put as links ? Will the initial ones work unchanged ? If you confirm, then the easiest is that I close this MR and do that separately. (The part touching |
So: can I simply remove the svg's from this repo ? Should I update the links or will they work as is ? |
|
They should work as is, assuming they are working currently. Like I said, the current build process isn't touching the SVGs in this repo at all. |
Since we haven't made progress in the last three years on #1887, I'm at least moving all images to a subdirectory to make things a bit clearer.