Skip to content

Commit

Permalink
Merge pull request ucsd-progsys#2145 from ucsd-progsys/fd/readme-groo…
Browse files Browse the repository at this point in the history 
…ming

Readme updates
  • Loading branch information
@facundominguez
facundominguez authored Feb 7, 2023
2 parents b655f29 + bbb2dd1 commit 9065611
Show file tree
Hide file tree
Showing 4 changed files with 17 additions and 108 deletions.
95 changes: 16 additions & 79 deletions README.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -107,28 +107,26 @@ For documentation on the `test-driver` executable itself, please refer to the
`README.md` in `tests/` or run `cabal run tests:test-driver -- --help` or `stack
run test-driver -- --help`

_For a way of running the test suite for multiple GHC versions, consult the General Development FAQs. below_

There are particular scripts for running LH in the different modes, e.g. for different
compiler versions. These scripts are in:

$ ./scripts/test

So you can run *all* the tests for say the ghc-8.10 version by
So you can run *all* the tests by

$ ./scripts/test/test_810_plugin.sh
$ ./scripts/test/test_plugin.sh

You can run a bunch of particular test-groups instead by

$ LIQUID_DEV_MODE=true ./scripts/test/test_810_plugin.sh <test-group-name1> <test-group-name2> ...
$ LIQUID_DEV_MODE=true ./scripts/test/test_plugin.sh <test-group-name1> <test-group-name2> ...

and you can list all the possible test options with

$ LIQUID_DEV_MODE=true ./scripts/test/test_810_plugin.sh --help
$ LIQUID_DEV_MODE=true ./scripts/test/test_plugin.sh --help

or get a list of just the test groups, one per line, with

$ LIQUID_DEV_MODE=true ./scripts/test/test_810_plugin.sh --show-all
$ LIQUID_DEV_MODE=true ./scripts/test/test_plugin.sh --show-all

To pass in specific parameters and run a subset of the tests, you can invoke cabal directly with

Expand All @@ -154,7 +152,7 @@ For details on adding tests, see note [Parallel_Tests] in `tests/test.hs`.

When `liquidhaskell` tests run, we can collect timing information with

$ ./scripts/test/test_810_plugin.sh --measure-timings
$ ./scripts/test/test_plugin.sh --measure-timings

Measures will be collected in `.dump-timings` files. These can be converted to json
data with
Expand Down Expand Up @@ -183,7 +181,7 @@ current directory.
The current formatting is optimized for comparing the outputs of running
the benchmarks alone.

$ scripts/test/test_810_plugin.sh \
$ scripts/test/test_plugin.sh \
benchmark-stitch-lh \
benchmark-bytestring \
benchmark-vector-algorithms \
Expand All @@ -192,75 +190,14 @@ the benchmarks alone.
benchmark-icfp15-pos \
benchmark-icfp15-neg

## How to Profile

See the instructions in [scripts/ProfilingDriver.hs][]

## How to Get Stack Traces On Exceptions

1. Build with profiling on

```
$ stack build liquidhaskell --fast --profile
```
2. Run with backtraces
```
$ liquid +RTS -xc -RTS foo.hs
```
```
stack exec -- liquid List00.hs +RTS -p -xc -RTS
```
## Working With Submodules
To update the `liquid-fixpoint` submodule, run:
```
cd ./liquid-fixpoint
git fetch --all
git checkout <remote>/<branch>
cd ..
```
This will update `liquid-fixpoint` to the latest version on `<branch>` (usually `master`)
from `<remote>` (usually `origin`). After updating `liquid-fixpoint`, make sure to include this change in a
commit! Running:
## Miscelaneous tasks

```
git add ./liquid-fixpoint
```
will save the current commit hash of `liquid-fixpoint` in your next commit to the `liquidhaskell` repository.
For the best experience, **don't** make changes directly to the `./liquid-fixpoint` submodule, or else git
may get confused. Do any `liquid-fixpoint` development inside a separate clone/copy elsewhere. If something
goes wrong, run:
```
rm -r ./liquid-fixpoint
git submodule update --init
```
to blow away your copy of the `liquid-fixpoint` submodule and revert to the last saved commit hash.
* **Profiling** See the instructions in [scripts/ProfilingDriver.hs][].
* **Getting stack traces on exceptions** See `-xc` flag in the [GHC user's guide][ghc-users-guide].
* **Working with submodules** See `man gitsubmodules` or the [git documentation site][git-documentation].

Want to work fully offline? `git` lets you add a local directory as a remote. Run:
```
cd ./liquid-fixpoint
git remote add local /path/to/your/fixpoint/clone
cd ..
```
Then to update the submodule from your local clone, you can run:
```
cd ./liquid-fixpoint
git fetch local
git checkout local/<branch>
cd ..
```
[ghc-users-guide]: https://downloads.haskell.org/ghc/latest/docs/users_guide/
[git-documentation]: https://git-scm.com/doc

## Releasing on Hackage

Expand Down Expand Up @@ -418,18 +355,18 @@ action by looking at the pattern synonym for [FunTy][].

Yes. The easiest way is to run one of the scripts inside the `scripts/test` directory. We provide scripts
to run the testsuite for a variety of GHC versions, mostly using `stack` but also with `cabal` (e.g.
`test_810_plugin.sh`). If run without arguments, the script will run the _full_ testsuite. If an argument
`test_plugin.sh`). If run without arguments, the script will run the _full_ testsuite. If an argument
is given, only a particular pattern/test will be run. Running

```
./scripts/test/test_810_plugin.sh BST
./scripts/test/test_plugin.sh BST
```

will run all the tests which name matches "BST". In case the "fast recompilation" is desired, it's totally
possibly to pass `LIQUID_DEV_MODE` to the script, for example:

```
LIQUID_DEV_MODE=true ./scripts/test/test_810_plugin.sh
LIQUID_DEV_MODE=true ./scripts/test/test_plugin.sh
```

[GHC.API]: https://github.com/ucsd-progsys/liquidhaskell/blob/develop/src/Language/Haskell/Liquid/GHC/API.hs
Expand Down
25 changes: 1 addition & 24 deletions scripts/plot-performance/README.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -5,27 +5,4 @@ produced by LH's testuite. It will produce something like this:

![perf-min](https://user-images.githubusercontent.com/442035/78143687-e3f4a480-742e-11ea-9a47-6b1800914a15.png)

### Usage

In order to measure, say, regression between two LH branches, it's first necessary to acquire two `.csv`
files to compare. For example, suppose you want to measure the performance changes between `develop` and
a `new-feature` branch. The easiest way is to do something like this:

```
git checkout develop
stack build
stack test -j1 liquidhaskell:test --flag liquidhaskell:include --flag liquidhaskell:devel --test-arguments="-p Micro"
git checkout new-feature
stack build
stack test -j1 liquidhaskell:test --flag liquidhaskell:include --flag liquidhaskell:devel --test-arguments="-p Micro"
```

After doing so, inside `tests/logs` you will find a bunch of folders named after your hostname, with some
timestamps. At that point you can simply do:

```
./chart_perf.sh ../path/to/develop.csv ../path/to/new_feature.csv
```

The order is _chronological_, i.e. the first csv should be the "before" and the second the "after". After
you do that, you should hopefully have a `perf.png` image on your filesystem to inspect.
See the main [README](../../README.md#how-to-create-performance-comparison-charts) for usage information.
5 changes: 0 additions & 5 deletions scripts/test/test_901_plugin.sh
View file

This file was deleted.

0 scripts/test/test_810_plugin.sh → scripts/test/test_plugin.sh
View file
File renamed without changes.

0 comments on commit 9065611

Please sign in to comment.