promising-coq icon indicating copy to clipboard operation
promising-coq copied to clipboard

Published 20 hours ago • verified publisher icon snu-sf

Add Documentation

Open alxest opened this issue 7 years ago • 4 comments

  • Add documentation for "imm"
  • Add documentation for "cmem"

alxest avatar Dec 16 '17 12:12 alxest

Would you please elaborate the documentation bugs you are reporting?

jeehoonkang avatar Dec 16 '17 12:12 jeehoonkang

  • In Memory.v's future_imm, it would be better to clarify what "imm" means.
  • In Makefile, it would be better to clarify what "cmem" means.

(@jeehoonkang said "imm" is "immediate" and "cmem" might be "c memory model")

alxest avatar Dec 16 '17 12:12 alxest

  • In Thread.v's promise_step, it would be better to clarify what pf means. Is it something like promise-free? I can find the definition (PF: pf = andb (Memory.op_kind_is_lower kind) (negb released)) but I can't think of its motivation (spec).

alxest avatar Dec 18 '17 02:12 alxest

  • In respectful5.v, it would be better to clarify what clo, rclo and grespectful means.

alxest avatar Dec 24 '17 09:12 alxest