wdk 0.5.3 README example malfunctions

[pnkfelix]

The README for wdk 0.5.3 (and perhaps earlier) has a "Run" section that says the following:

With the `PATH` setup correctly, you should be able to run the `wy` tool
to compile Whiley programs as follows:

    % cd examples
    % wy compile hello-world.whiley

When I tried to follow these instructions, I encountered a few problems.

First: The instructions say to go into an examples/ directory. But, perhaps due to a typo, there is no such directory. There is an example/ directory.

Second: Once in the example/ directory, running wy compile hello-world.whiley produces the following result:

wdk-v0.5.3/example % wy compile hello-world.whiley
Internal failure: Index 0 out of bounds for length 0

To be fair, the example/ directory does not have any file named hello-world.whiley. There is a source file example/src/main.whiley...

Third: Even if one does attempt wy compile src/main.whiley from that example/ directory, you still get the same Internal failure.

(Was the README written for a different source code repository or something?)

[DavePearce]

Hey Felix,

Yes, you are right the documentation is out-of-date --- sorry about that. I will try to update it shortly! The easiest way to try Whiley right now is through whileylabs. To get the WDK setup, here are the minimal steps:

1. Create fresh directory for project (e.g. test)
2. Create fresh subdirectory src (e.g. test/src)
3. Create file test/wy.toml with this:

   
   [package]
   name="test"

[build] platforms=["whiley"]

4. Create example file (e.g. `test/src/main.whiley`) such as:
```whiley
public method main():
   assert false

5. At this point, running wy build should produce a file test/bin/test.wyil

At this point, we can now enable verification by adding the following to our wy.toml file:

[build.whiley]
verify=true

And running wy build again should produce an error indicating the assertion failed. A few caveats:

1. (Boogie/Z3) Enabling verification as above uses Whiley's internal verifier (i.e. not Boogie/Z3). This is easier to get going with, but is not very powerful. To use Boogie/Z3 you need to install Boogie and then add boogie as a platform after whiley in wy.toml
2. (Dependencies) In principles you can add dependencies (e.g. the standard library) in the wy.toml file. Unfortunately, I'm in the middle of changes which meant some binary incompatibility. So, I don't think dependencies will work for you. I obviously need to figure out a migration approach for this kind of thing.

[DavePearce]

I should add, great that you're interested in trying out Whiley!! Do not hesitate to post questions here, or even email me directly. A few examples you might find interesting to look at:

1. (Conway) https://github.com/DavePearce/Conway.wy
2. (Minesweeper) https://github.com/DavePearce/Minesweeper.wy
3. (Standard Library) https://github.com/Whiley/STD.wy

[pnkfelix]

Thanks @DavePearce !

[DavePearce]

Hey @pnkfelix,

Thought you might be interested in this:

cargo install whiley

Its very rough at this stage, but tested on Mac and Linux. To do anything useful you need a minimum project (as above). It requires java to be installed somewhere, as it is basically just a wrapper for the existing java codebase. However, my plan is to migrate the Whiley compiler from Java into Rust over the course of the next year.

[DavePearce]

Right, am closing this issue now as it no longer applies to the latest released version v0.6.1 which now uses cargo as the primary deployment mechanism. See here.