[K-Bug] Two configuration declarations in a single module produces an unhelpful error message

[sskeirik]

What component is the issue in?

Front-End

Which command

• kompile
• kast
• krun
• kprove
• kprovex
• ksearch

What K Version?

v7.1.170-0-g5c84d48f69

Operating System

Linux

K Definitions (If Possible)

module TMP
  imports INT
  configuration <extraLocalConfig> 1 </extraLocalConfig>
  configuration <mainConfig> <extraLocalConfig/> </mainConfig>
endmodule

Steps to Reproduce

Save above definition to tmp.k and run kompile tmp.k.

An error message of the form below will be emitted:

[Error] Compiler: Malformed external cell in configuration declaration.
        Source(/home/stephen/rv/tmp.k)
        Location(4,30,4,49)
        4 |       configuration <mainConfig> <extraLocalConfig/> </mainConfig>
          .                                  ^~~~~~~~~~~~~~~~~~~
[Error] Compiler: Had 1 parsing errors.

Expected Results

I expect to get an error that says something like:

A module may only have up to one configuration declaration; please merge the two configuration declarations into one (or) put the two configuration declarations into separate modules.

I just made this on the fly --- there is definitely a better way to word it, but this is just for a start.

[dwightguth]

The original proposed solution here was to report an error if the module contained more than one configuration declaration. However, this explicitly contradicts the solution of #2075 . A better solution is probably simply to update the text of the error message that is already being reported with a bit more detail about possible causes. However, I am inclined to leave this on the backlog for now since we were able to identify the cause of the issue Stephen was having and it is no longer blocking.