Pin all GitHub Actions to SHAs

[fyliu]

Fixes #676

What changes did you make?

• added script (AI-generated) to pin all GitHub Actions to commit SHAs
• updated workflows to use commit SHAs
• added documentation for the new script

Why did you make the changes (we will use this info to test)?

• SHA-pinning is for security, because the action tags can be re-pointed to malicious commits.
• I had to reorganize the scripts documentation into a folder structure in order to add a page for the script.
• I figured it's okay to let AI create the script, since it makes small changes that we would look at before committing.

Testing

• Change .github/workflows/deploy-docs.yml - uses: actions/checkout@... line to - uses actions/checkout@v4 and run the script to see that it writes the SHA for it.

[fyliu]

Pushed a fix for the 4 documentation links warnings.

Suggested changes

Switch autolinks to awesome-links

I'm looking at the autolinks plugin for mkdocs and it doesn't work very well with the awesome-pages plugin. The problem is it doesn't support multiple files named index.md in different directories, so I ended up specifying the full relative path, which defeats the purpose of the plugin.

There's another plugin called awesome-links that supports partial paths such as scripts/index.md and tools/index.md, which is better than autolinks

Update awesome-pages to awesome-nav

Looks like awesome-pages got renamed to awesome-nav, so we should probably switch to that too.

[fyliu]

Pushed a fix for the 4 documentation links warnings.

Suggested changes

Switch autolinks to awesome-links

I'm looking at the autolinks plugin for mkdocs and it doesn't work very well with the awesome-pages plugin. The problem is it doesn't support multiple files named index.md in different directories, so I ended up specifying the full relative path, which defeats the purpose of the plugin.

There's another plugin called awesome-links that supports partial paths such as scripts/index.md and tools/index.md, which is better than autolinks

Update awesome-pages to awesome-nav

Looks like awesome-pages got renamed to awesome-nav, so we should probably switch to that too. The 2 awesome plugins are by the same developer, which explains why they work well together.