search

achlipala / frap

Formal Reasoning About Programs
Other
665 stars 83 forks source link

Add TransitionSystems.vo to 'lib' target #35

Closed Michael137 closed 4 years ago

Michael137 commented 4 years ago

ModelChecking.v imports the TransitionSystems module. This currently fails with: "Unable to locate library TransitionSystems. (While searching for .vos file)"

Adding TransitionSystems.vo to the 'lib' target ensures that ModelChecking.v's imports resolve

Michael137 commented 4 years ago

Alternatively can build whole book

achlipala commented 4 years ago

Actually, both TransitionSystems and ModelChecking are chapters of the book, not intended to be relied on anywhere else, though the latter does reference the former. Is there some inconsistent code giving the impression either belongs in the library?