ktest -- unexpected option overriding behavior

[yilongli]

Just go to tutorial/1_k/4_imp++/lesson_6 in unified-builtins2 branch and run ktest tests/config.xml. Then you can see the definition is kompiled twice for the maude backend, while the intent here was to test both the Java and maude backends.

@dwightguth believes this is because the kompile-option specified in the lesson_6/tests/config.xml somehow overrides the kompile-options in 2_imp/lesson_1/tests/config.xml.

@osa1 Omer, I am assigning this issue to you. Thanks.

[osa1]

Interesting. It seems like not only --backend option but also --directory option is missing here: (specified in 2_imp/lessson_1/tests/config.xml)

Kompile the language definitions...(2 in total)
Done with ['/home/omer/K/k_new_dist/k/bin/kompile' '/home/omer/K/k_new_dist/k/tutorial/1_k/4_imp++/lesson_6/imp.k' '--transition' 'lookup increment assignment read print'] (time 31004 ms)
Done with ['/home/omer/K/k_new_dist/k/bin/kompile' '/home/omer/K/k_new_dist/k/tutorial/1_k/4_imp++/lesson_6/imp.k' '--transition' 'lookup increment assignment read print'] (time 32492 ms)
SUCCESS

(--directory option is also missing in krun commands, again specified in same config file)

@yilongli can you please confirm that I'm looking to correct config file?

[osa1]

@yilongli your branch is missing some ktest patches. Can you rebase your branch on current master?

[osa1]

@yilongli btw, what you're expecting from ktest is not how it's supposed to work. When you have something like:

  <include file="...">
    <kompile-option name="..." value="..." />

It overrides kompile options parsed in included file, does not extend it. If I understand the issue here correctly, you're expecting it to extend the parsed kompile options, right?

@daejunpark can you confirm that overriding kompile options in the included file is how ktest is designed and it's not a bug?

[daejunpark]

@yilongli @osa1

Omer is right.

All of kompile/krun options such as <kompile-option>, <all-programs>, <program> elements in <include> overwrite the included counterparts. That is, this behavior is not a bug but a design.

The rational of this design is that it will be too difficult for users to keep track of all those options when we allow them to be extended. It would be much tricker when some of extended options are conflicted with the previous ones. In that case, we will need a way to describe how to resolve those conflict, which will make ktest much more complex.

Note that such an extension is only allowed in more-programs and more-results which extend the previous programs and results attributes. They cannot have a conflict, because it only add the more-programs/results to the previous programs/results.

Of course, I admit that this design is not consistent in some sense, although it is our best at that moment. It will be great if you suggest a more general and simpler design.

By the way, I'm sorry not to explain this in the manual to-be-processed.txt. I'll add it.

[grosu]

While I am with Deaujun here that you should propose simpler designs if you can, I am also stressing the fact that we have spent weeks designing the current version to work well with the tutorial and the exercises in the tutorial. So before you think for 5 seconds and propose something, please take a look at the uses of ktest both in the tutorial AND in the exercises in the tutorial. I mean, students are asked to extend languages in the tutorial with certain features, and the config.xml files for those are already given. The current design a consequence of a lot of suffering and adjusing until we found a good compromise. So make sure you understand all those issues that ktest tried to resolve first and keep it in mind there there is more than one possible use of ktest. Daejun, you may want to search a but through issues and add also comments like this to the to-be-processed file, because they will help us write up the ktest section (or chapter?) in the manual.

[yilongli]

@osa1 Thank you, Omer. I didn't realize your patch is on the master branch since most of the development recently happens in the unified-builtins2. I will try to incorporate your recent patch.

@osa1 @daejunpark I am perfectly fine with the current design as long as it's well explained.

[dwightguth]

@grosu: to be clear, the current design will require Yilong to significantly rewrite the xml files in the tutorial to make them somewhat less modular. The cleanest thing to do, I believe, is to have two xml files per lesson, one for maude and one for java. then he will have to aggregate them together at the higher level directories. This is the way it will have to be any time we are compiling more than one backend of the same definition, and overriding kompile or krun options in another file. If you're fine with that, then yes, we can proceed forward without changing ktest. But I want to make sure you're aware that that is a consequence if we leave the current design unchanged.

On Thu, Jun 5, 2014 at 12:36 AM, Yilong Li notifications@github.com wrote:

@osa1 https://github.com/osa1 Thank you, Omer. I didn't realize your patch is on the master branch since most of the development recently happens in the unified-builtins2. I will try to incorporate your recent patch.

@osa1 https://github.com/osa1 @daejunpark https://github.com/daejunpark I am perfectly fine with the current design as long as it's well explained.

— Reply to this email directly or view it on GitHub https://github.com/kframework/k/issues/545#issuecomment-45182641.

[grosu]

It is OK to have two different config.xml files, one for each backend. We can call them config-maude.xml and config-java.xml, and then we can also have a config.xml in the same folder which includes both. That is, we do not need to aggregate them at higher level directories. This way, we can still call ktest tests/config.xml in each folder in order to "test everything".

[dwightguth]

Alright, although you'll still have boilerplate in every diretory combining the two files into a third. But maybe you're fine with that too.

On Mon, Jun 9, 2014 at 7:14 PM, Grigore Rosu notifications@github.com wrote:

It is OK to have two different config.xml files, one for each backend. We can call them config-maude.xml and config-java.xml, and then we can also have a config.xml in the same folder which includes both. That is, we do not need to aggregate them at higher level directories. This way, we can still call ktest tests/config.xml in each folder in order to "test everything".

— Reply to this email directly or view it on GitHub https://github.com/kframework/k/issues/545#issuecomment-45560374.

[grosu]

But the boilerplate does not seem to be avoided anyway, because you would need to have it in the parent directory. Maybe you can push it all the way to the top, so you would have the boilerplate only once at the top, but in that case you would need to call ktest twice in each lesson to test it individually. So far, modularizing ktesting the way it is in the tutorial, that is, to have a tests/config.xml file in each folder "testing everything", served us well, so I would be in favor of keeping it. Also, if everything goes well, the config.xml file should really one contain two lines, one including config-maude.xml and the other including xonfig-java.xml.

Grigore

---

From: dwightguth [notifications@github.com] Sent: Monday, June 09, 2014 7:23 PM To: kframework/k Cc: Rosu, Grigore Subject: Re: [k] ktest -- unexpected option overriding behavior (#545)

Alright, although you'll still have boilerplate in every diretory combining the two files into a third. But maybe you're fine with that too.

On Mon, Jun 9, 2014 at 7:14 PM, Grigore Rosu notifications@github.com wrote:

It is OK to have two different config.xml files, one for each backend. We can call them config-maude.xml and config-java.xml, and then we can also have a config.xml in the same folder which includes both. That is, we do not need to aggregate them at higher level directories. This way, we can still call ktest tests/config.xml in each folder in order to "test everything".

— Reply to this email directly or view it on GitHub https://github.com/kframework/k/issues/545#issuecomment-45560374.

— Reply to this email directly or view it on GitHubhttps://github.com/kframework/k/issues/545#issuecomment-45560893.

[cos]

Site note: Regarding overriding behavior, when you have time, have a look at: https://github.com/typesafehub/config