IntersectMBO / IntersectMBO/formal-ledger-specifications
Fix instructions for plotting type-checking times
- Dominant language
- Agda
- Stars
- 52
- Forks
- 20
- Avg merge
- 6d 14h
- Merged PRs (30d)
- 7
Description
The instructions on the CONTRIBUTING page for generating type-checking times don't work.
For example,
```
❯ python scripts/plot_typecheck_time.py > index.html
zsh: command not found: python
```
Apparently, we're assuming users have python installed and in the current path, so let's try it inside the `mkdocs` derivation.
```
❯ nix develop .#mkdocs
(base) $ python scripts/plot_typecheck_time.py > index.html
/nix/store/cfapjd2rvqrpry4grb0kljnp8bvnvfxz-python3-3.13.8/bin/python: can't open file '//scripts/plot_typecheck_time.py': [Errno 2] No such file or directory
```
It seems we're assuming the user is somehow already in the `build-tools` directory, so let's try `python build-tools/scripts/plot_typecheck_time.py > index.html`:
```
❯ nix develop .#mkdocs
(base) $ python build-tools/scripts/plot_typecheck_time.py > index.html
Traceback (most recent call last):
File "/home/williamdemeo/git/IO/fls/william/965-refactor-ledger-properties/build-tools/scripts/plot_typecheck_time.py", line 4, in
import pandas as pd
ModuleNotFoundError: No module named 'pandas'
```
It seems the script needs pandas, so we should put that and anything else the type-checking plotting script requires, in a nix derivation and tell users to invoke that shell before running `python build-tools/scripts/plot_typecheck_time.py > index.html`.
Contributor guide
Assessment
This issue has not been assessed yet.