Command Reference¶

This page collects the commands most users actually need.

Build and Test¶

lake build
python3 -m unittest discover -s tests

Inspect Available Scenarios and Algorithms¶

python3 -m vpp_rl.train --list-scenarios
python3 -m vpp_rl.train --list-algorithms

Export a Lean Rule Table¶

python3 -m vpp_rl.rule_table \
  --scenario peak_shaving \
  --output artifacts/peak_shaving_shield_table.json

Train and Export a Trace¶

No shield:

python3 -m vpp_rl.train \
  --episodes 180 \
  --algorithm double_q \
  --scenario peak_shaving \
  --shield-mode none \
  --output artifacts/peak_shaving_double_q_none_trace.json

Projection shield:

python3 -m vpp_rl.train \
  --episodes 180 \
  --algorithm double_q \
  --scenario peak_shaving \
  --shield-mode project \
  --output artifacts/peak_shaving_double_q_project_trace.json

Lean table-driven shield:

python3 -m vpp_rl.train \
  --episodes 180 \
  --algorithm double_q \
  --scenario peak_shaving \
  --shield-mode table_project \
  --shield-table artifacts/peak_shaving_shield_table.json \
  --output artifacts/peak_shaving_double_q_table_project_trace.json

Verify a Trace in Lean¶

lake env lean --run VppLeanRl/Cli.lean -- \
  artifacts/peak_shaving_double_q_table_project_trace.json

Run the Full Demo¶

./scripts/run_demo.sh 180 double_q peak_shaving table_project

Arguments:

episodes
algorithm
scenario
shield_mode

Serve the Documentation Site¶

Install the docs dependency:

python3 -m pip install -r docs/requirements.txt

Start the local docs server:

mkdocs serve

Start the Chinese docs server:

mkdocs serve -f mkdocs.zh.yml

Build the full bilingual site:

./scripts/build_docs_site.sh

Useful Files¶

scripts/run_demo.sh
vpp_rl/train.py
vpp_rl/rule_table.py
VppLeanRl/Cli.lean
VppLeanRl/Trace.lean