Switch to Dune

[alberdingk-thijm]

This PR resolves issue #4. Expect it to break lots of namespacing.

You can now compile the project using dune build src/exe/main.exe, which saves the executable to _build/src/exe/main.exe.

Testing support with Dune still needs to be added. This PR breaks the existing build system.

[alberdingk-thijm]

I am concerned about the fact that now we have to prefix all of our modules by their location in the file hierarchy -- I think it's very important to be able to tell what code is doing at a glance, and this can add visual clutter which makes that harder. I'd also rather not be thinking about a file's location in the hierarchy when I'm using functions from that file. Most of my concerns can be solved by judicious use of open and let open, however, so I'm not too worried. We may have to discuss open hygiene more in the future if it continues to be a problem.

This is a fair point. On the other hand, there are cases where having the namespacing can clarify what a file is doing, and also makes it easier to know where to look for the code when debugging or looking for particular files. The new structure contributes to some rather unwieldy names, but these can be changed with a simple set of refactorings once we discuss them further. I want to change Nv_core to Nv_lang, for one, or perhaps Nv.Lang.

The question of which files should be opened relates to #5. nv_datatypes and nv_datastructures export some fairly basic commonly-used types, so in most cases it makes sense to just put open Nv_datatypes and open Nv_datastructures at the top of a file and go from there. We want to minimize how many times a programmer tries to write a line like Syntax.aeval only to realize they don't have Nv_core open, and then to have to look at the directory structure to figure out where Syntax is stored (which invalidates the whole original purpose of using namespacing to make it obvious where things are).

We currently have many more directories than most dune projects, which contributes to this problem. It would be worth looking at merging some directories to reduce the number of open statements in the code. We may also want to consider using more nesting in some places if certain code is rarely modified or not used directly from the binary, following the typical way libraries provide APIs to binaries.

[nickgian]

Can't wait for this, I want it to get my dynamic linking to work!

What's the problem with opens though? Merlin allows you to jump to the location of a definition so I don't really need to prefix every function call to navigate the code.

Regarding file structure, I think it's common to have folders like this. I'd like to see datatype and datastructures merged though, there is no need for them to be different and I never seem to be able to remember what files each of them are supposed to hold. Other changes I would do to the file structure: move OptimizeBranches.ml, Failures.ml, Slicing.ml to transformations, make a new compression folder and move Abstraction and AbstractionMap there, make a folder QuickCheck and move QuickCheck and utils/Generators in there. I can do the changes above to the folder structure if you want, it may be a good idea to do them before merging.

[alberdingk-thijm]

I think those folder changes should work; datatypes and datastructures could certainly merge into something like types. If Nv_utils.Visitors moves to lang and Nv_utils.Generators moves to QuickCheck, then we can get rid of the utils folder. You're welcome to pull the branch and perform that reorganization, @nickgian; just be sure to dune build afterwards to make sure nothing breaks.

The namespacing/open usage partly comes down to a question of personal taste/style: for instance, if the namespace is explicit then we can be more succinct with the module's methods; instead of

Nv_solution.Solution.print_solution sol

we could do

open Nv_solution;;
Solution.print sol

or have Nv_solution re-export Solution.print as print_solution and do:

Nv_solution.print_solution sol

In my mind, what is nicest is having a structure where we:

1. only open a module where we make extensive use of its methods
2. use re-exporting to make it easy to skip referencing intermediate parts
3. avoid having to open a module just to use one very handy method (where it may instead be better for that method to go somewhere else)

The code at present does not really take advantage of namespacing anywhere. For instance, lang and smt both have Lexer and Parser files, but the smt files are all prefixed by "Smt", which could be changed to using the SMT files only within smt and then calling them using Smt.Utils and so forth. Here is a blog post discussing how to avoid prefixes and suffixes that clutter the namespace in this way.

[DKLoehr]

I'd also support merging datastructures and datatypes -- I also find myself getting confused as to which modules are in each. Moving Visitors to lang also makes sense. I trust Nick's recommendations for the other changes.

I'm not sure about getting rid of the utils folder, though -- I'd like to put OCamlUtils and Collections in there (though this will require splitting off the collections that depend on Syntax from those that don't). RecordUtils should also go there.

I think we also need to get testing working before we can consider this completed. I think that in order to do that we'd need to pull Main_defs and Wellformed out of src/exe, since they need to be accessible to our testing system (which doesn't use the final executable itself).

I think my personal preference leans strongly away from using the file system for namespacing. The main use of the file system in my mind is to allow people to locate files using semantic knowledge about the files' contents. I'd prefer to disambiguate modules by their names (SmtUtils, as opposed to Nv_smt.Utils) -- having multiple files named "Utils" which are distinguished solely by position in the filesystem seems ripe for confusion. This is definitely a preference thing, however.

There are also going to be certain libraries -- lang is the most obvious -- which will be heavily used in just about every file that depends on them, so we'll probably just end up opening a bunch of them at the top regardless.

[DKLoehr]

I made some of the changes discussed above, and...moving files around is an enormous headache now. Granted, I was working on some files which lots of things depend on, but still. I think that's another incentive to get everything right the first time.

To (hopefully) aid with that, I created a hacky little python script which prints dependencies for each file AND each folder. It can be restricted to only print dependencies on dune libraries (i.e. folders) instead of all dependencies. Hopefully it will make it easier to figure out what depends on what when we're deciding if/where to move things.

Edit: Also, the compiler currently spits out huge numbers of warnings. I'm all for stricter warning practices -- we've been pretty lax so far -- but we should probably deal with the existing ones before we merge. Some will probably be easy to deal with, but others (e.g. unused variables in really complicated expressions) will probably be pretty tricky.

[DKLoehr]

I made some more changes: merging datatypes and datastructures as discussed, and moving Profile into utils instead of smt. Having done that, I think we should consider moving Var and Integers from datastructures to utils. They both have no external dependencies, and there are several files which depend on datastructures only so they can use one of those two. I think there's an argument to be made that they're both generic "utilities" (arbitrary-size integers and easy-to-disambiguate variables) to justify their location, although my main reasoning is practical.

I have also been looking at the various warnings that dune currently emits. In addition to the currently-disabled warnings, I think we should disable the following ones:

• Warning 9: Incomplete record patterns. I'm not concerned about these because if someone forgets to match a field and later needs that information, they won't have any option but to add it into the pattern. So there's not too big a chance for writing incorrect code.
  • Warning 40: Constructors used outside of scope. I'm not worried about these because they rely on typing information, which can be easily viewed with merlin and used to locate the original scope if needed. Furthermore, we're pretty good about not having name conflicts between constructors.
  • Warning 42: Type-directed disambiguation. My understanding is that this has been a feature of OCaml for a while and is pretty stable -- the only reason to enable this warning is if we wanted backwards-compatibility with older compilers, and I don't see any need for that.
  • Warning 45: Opening modules which contains variants/records with the same constructor names/labels. The only way around this would be to rename some of our types (e.g. by prefixing all the constructors) or use a large number of module prefixes. In some cases using only local opens might be able to fix it. As far as I can tell, the worst that can come out of disabling the warning is a confusing type error, so I think we just don't spend the extra effort changing existing types around.

Warnings that I think we should definitely keep:

• Warning 27: Unused variables. Although there are some good reasons for something like naming unused arguments of functions (to e.g. tell the reader what that argument represents), this warning is really useful for detecting accidental shadowing of variable names, and is also useful for helping the developer make sure they actually use the results of their previous computations.
• Warning 60: Unused modules. I wouldn't expect this to come up much, but we actually had several hits. I think it's handy to keep around just to have less cluttered code.
• Warning 66: Unused opens. Also handy to have around, it can make dependencies cleaner and make the code a little less cluttered.