IntersectMBO / IntersectMBO/formal-ledger-specifications

Fix instructions for plotting type-checking times

Open
#982 0 comments 0 reactions 1 assignee Claimed by @carlostome View on GitHub
documentation
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

Open the contributing guide

Assessment

This issue has not been assessed yet.

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.