Closed andrey-kuprianov closed 1 year ago
The choice of a config file format is not simple.
Having ruled out the TOML/YAML, and having recognised the need for more flexibility, these seems to be the main alternatives:
Here are a couple of comparisons between different alternatives:
I am very much in favour of using Jsonnet. Here are the reasons:
hermeticity
principle is very important for test reproducibility
As it occurs to me, we will be also able to use the Rust Jsonnet implementation above (probably a fork with slight tweaking) as a replacement for our homegrown Jsonatr tool. Here is why:
A few words in favor of Dhall:
That said, like many of these cases, given the more familiar syntax and OOP features, I imagine the initial learning curve for Jsonnet is gentler (but would not be surprised if you pay for it later, due to turing completeness and complexity of object inheritance).
wow, @shonfeder thanks for commenting on this:)
Those are good points. But I think one of the most important points is that the learning curve should be as flat as possible. Having pure JSON as the entry point is perfect for that.
Another thing, as far as I understand about Dhall, is that everything needs to be typed. There is a huge obstacle if e.g. we want to process Apalache counterexample, i.e. import it, and extract smth. from it. Try to define types for TLA+ in Dhall;)
Also, as far as I understand, importing JSON in Dhall is not even implemented yet, though people are asking about this already for 2+ years now. Seems not possible to do. In Jsonnet this is trivial.
Honestly, I don't care too much about theoretical correctness provided by the language itself. I care much more about its practicality. At the end, it is we who are mostly going to write code for these tools, so we can take care of the correctness by good design and simplicity -- this is our speciality.
Also, doesn't hurt if we pursue different approaches for Themis-Tracer and MBT; it's even good if we can compare them.
Dhall is not a serialization format and is not designed to be machine writeable, so if what you need is something you can generate programmatically, I totally agree Dhall is not the right choice.
But I'd encourage differentiating configuration from serialization. Expecting to have one format that is both a serialization for communicating between machines and a human-focused configuration language is a bad idea IMO. Whether you go with Dhall or Jasonnet or something else, I think trying to use the same format for both data exchange and human config will end up leading to pain.
Honestly, I don't care too much about theoretical correctness provided by the language itself. I care much more about its practicality. At the end, it is we who are mostly going to write code for these tools, so we can take care of the correctness by good design and simplicity -- this is our speciality.
I disagree on this point almost entirely, but that is out of band :)
I agree there's no need for uniformity between completely unrelated projects :)
We need to design a configuration format to describe model-based tests.
The config format should provide the fields to specify: