рдпрд╣ рдХрдорд╛рдВрдб coqchk.opt рд╣реИ рдЬрд┐рд╕реЗ рд╣рдорд╛рд░реЗ рдХрдИ рдореБрдлреНрдд рдСрдирд▓рд╛рдЗрди рд╡рд░реНрдХрд╕реНрдЯреЗрд╢рди рдЬреИрд╕реЗ рдХрд┐ рдЙрдмрдВрдЯреВ рдСрдирд▓рд╛рдЗрди, рдлреЗрдбреЛрд░рд╛ рдСрдирд▓рд╛рдЗрди, рд╡рд┐рдВрдбреЛрдЬ рдСрдирд▓рд╛рдЗрди рдПрдореБрд▓реЗрдЯрд░ рдпрд╛ рдореИрдХ рдУрдПрд╕ рдСрдирд▓рд╛рдЗрди рдПрдореБрд▓реЗрдЯрд░ рдХрд╛ рдЙрдкрдпреЛрдЧ рдХрд░рдХреЗ рдСрдирд╡рд░реНрдХреНрд╕ рдлреНрд░реА рд╣реЛрд╕реНрдЯрд┐рдВрдЧ рдкреНрд░рджрд╛рддрд╛ рдореЗрдВ рдЪрд▓рд╛рдпрд╛ рдЬрд╛ рд╕рдХрддрд╛ рд╣реИред
рдХрд╛рд░реНрдпрдХреНрд░рдо:
рдирд╛рдо
coqchk - Coq рдкреНрд░реВрдл рдЪреЗрдХрд░ рд╕рдВрдХрд▓рд┐рдд рдкреБрд╕реНрддрдХрд╛рд▓рдп рд╕рддреНрдпрд╛рдкрдирдХрд░реНрддрд╛
SYNOPSIS
coqchk [ рд╡рд┐рдХрд▓реНрдкреЛрдВ ] рдореЙрдбреНрдпреВрд▓
рд╡рд░реНрдгрди
coqchk рд╕рдВрдХрд▓рд┐рдд рдкреБрд╕реНрддрдХрд╛рд▓рдпреЛрдВ (coqc рджреНрд╡рд╛рд░рд╛ рдирд┐рд░реНрдорд┐рдд .vo рдлрд╝рд╛рдЗрд▓реЗрдВ) рдХрд╛ рд╕реНрдЯреИрдВрдбрдЕрд▓реЛрди рдЪреЗрдХрд░ рд╣реИ
рдХреЙрдХ рдкреНрд░реВрдл рд╕рд╣рд╛рдпрдХ. рдЕрдзрд┐рдХ рдЬрд╛рдирдХрд╛рд░реА рдХреЗ рд▓рд┐рдП рд╕рдВрджрд░реНрдн рдореИрдиреБрдЕрд▓ рджреЗрдЦреЗрдВред рдпрд╣ рд╕рд╛рде рд▓реМрдЯрддрд╛ рд╣реИ
рдпрджрд┐ рд╕рднреА рдЕрдиреБрд░реЛрдзрд┐рдд рдХрд╛рд░реНрдп рд╕рдлрд▓ рд╣реЛ рдЧрдП рддреЛ рдирд┐рдХрд╛рд╕ рдХреЛрдб 0ред рдПрдХ рдЧреИрд░-рд╢реВрдиреНрдп рд░рд┐рдЯрд░реНрди рдХреЛрдб рдХрд╛ рдорддрд▓рдм рдпрд╣ рд╣реИ
рдХреБрдЫ рдЧрд▓рдд рд╣реЛ рдЧрдпрд╛: рдХреБрдЫ рд▓рд╛рдЗрдмреНрд░реЗрд░реА рдирд╣реАрдВ рдорд┐рд▓реА, рджреВрд╖рд┐рдд рд╕рд╛рдордЧреНрд░реА, рдЯрд╛рдЗрдк-рдЪреЗрдХрд┐рдВрдЧ
рдЕрд╕рдлрд▓рддрд╛, рдЖрджрд┐ред
рдореЙрдбреНрдпреВрд▓ рдЬрд╛рдВрдЪреЗ рдЬрд╛рдиреЗ рд╡рд╛рд▓реЗ рдореЙрдбреНрдпреВрд▓ рдХреА рдПрдХ рд╕реВрдЪреА рд╣реИред рдореЙрдбреНрдпреВрд▓ рдХреЛ рд╕рдВрдХреНрд╖рд┐рдкреНрдд рдпрд╛ рджреНрд╡рд╛рд░рд╛ рд╕рдВрджрд░реНрднрд┐рдд рдХрд┐рдпрд╛ рдЬрд╛ рд╕рдХрддрд╛ рд╣реИ
рдпреЛрдЧреНрдп рдирд╛рдо.
рд╡рд┐рдХрд▓реНрдк
-I рдбреАрдЖрдИрдЖрд░, --рд╢рд╛рдорд┐рд▓ рджреАрд░
рдирд┐рд░реНрджреЗрд╢рд┐рдХрд╛ рдЬреЛрдбрд╝реЗрдВ рджреАрд░ рд╢рд╛рдорд┐рд▓ рдкрде рдореЗрдВ
-R рджреАрд░ рдХреЛрдХрджрд┐рд░
рднреМрддрд┐рдХ рд░реВрдк рд╕реЗ рдкреБрдирд░рд╛рд╡рд░реНрддреА рдорд╛рдирдЪрд┐рддреНрд░рдг рдХрд░реЗрдВ рджреАрд░ рддрд╛рд░реНрдХрд┐рдХ рдХрд░рдиреЗ рдХреЗ рд▓рд┐рдП рдХреЛрдХрджрд┐рд░
-рд╕рдВрддрд╛рди
Coqchk рдХреЛ рдХрдо рдХреНрд░рд┐рдпрд╛рд╢реАрд▓ рдмрдирд╛рддрд╛ рд╣реИред
-рд╕реНрд╡реАрдХрд╛рд░ рдХрд░рддреЗ рд╣реИрдВ рдореЙрдбреНрдпреВрд▓
рдирд┐рд░реНрджрд┐рд╖реНрдЯ рдореЙрдбреНрдпреВрд▓ рдФрд░ рдЙрд╕рдХреА рд╕рднреА рдирд┐рд░реНрднрд░рддрд╛рдУрдВ рдХреЛ рд╡рд┐рд╢реНрд╡рд╕рдиреАрдп рдХреЗ рд░реВрдк рдореЗрдВ рдЯреИрдЧ рдХрд░реЗрдВ, рдФрд░ рдирд╣реАрдВ рдХрд┐рдпрд╛ рдЬрд╛рдПрдЧрд╛
рджреЛрдмрд╛рд░рд╛ рдЬрд╛рдБрдЪ рдХреА рдЧрдИ, рдЬрдм рддрдХ рдХрд┐ рдЕрдиреНрдп рд╡рд┐рдХрд▓реНрдкреЛрдВ рджреНрд╡рд╛рд░рд╛ рд╕реНрдкрд╖реНрдЯ рд░реВрдк рд╕реЗ рдЕрдиреБрд░реЛрдз рди рдХрд┐рдпрд╛ рдЧрдпрд╛ рд╣реЛред
-рдиреЛрд░реЗрдХ рдореЙрдбреНрдпреВрд▓
рдирд┐рд░реНрджрд┐рд╖реНрдЯ рдХрд░рддрд╛ рд╣реИ рдХрд┐ рджрд┐рдП рдЧрдП рдореЙрдбреНрдпреВрд▓ рдХреЛ рдЙрд╕рдХреА рдЬрд╛рдВрдЪ рдХрд░рдиреЗ рдХрд╛ рдЕрдиреБрд░реЛрдз рдХрд┐рдП рдмрд┐рдирд╛ рд╕рддреНрдпрд╛рдкрд┐рдд рдХрд┐рдпрд╛ рдЬрд╛рдПрдЧрд╛
рдирд┐рд░реНрднрд░рддрд╛ред
-рдПрдо, --рдпрд╛рдж
рдЪреЗрдХрд░ рджреНрд╡рд╛рд░рд╛ рдЙрдкрдпреЛрдЧ рдХреА рдЧрдИ рдореЗрдореЛрд░реА рдХрд╛ рд╕рд╛рд░рд╛рдВрд╢ рдкреНрд░рджрд░реНрд╢рд┐рдд рдХрд░рддрд╛ рд╣реИред
-рдУ, --рдЖрдЙрдЯрдкреБрдЯ-рд╕рдВрджрд░реНрдн
рд╕рддреНрдпрд╛рдкрд┐рдд рдХреА рдЧрдИ рддрд╛рд░реНрдХрд┐рдХ рд╕рд╛рдордЧреНрд░реА рдХрд╛ рд╕рд╛рд░рд╛рдВрд╢ рдкреНрд░рджрд░реНрд╢рд┐рдд рдХрд░рддрд╛ рд╣реИ: рдзрд╛рд░рдгрд╛рдПрдБ рдФрд░
рдЕрд╕рдВрд╡реЗрджрдирд╢реАрд▓рддрд╛ рдХрд╛ рдЙрдкрдпреЛрдЧ.
-рдЕрдкреНрд░рддреНрдпрд╛рд╢рд┐рдд-рд╕реЗрдЯ
рдЪреЗрдХрд░ рдХреЛ рдЙрди рдкреБрд╕реНрддрдХрд╛рд▓рдпреЛрдВ рдХреЛ рд╕реНрд╡реАрдХрд╛рд░ рдХрд░рдиреЗ рдХреА рдЕрдиреБрдорддрд┐ рджреЗрддрд╛ рд╣реИ рдЬрд┐рдиреНрд╣реЗрдВ рдЗрд╕ рдзреНрд╡рдЬ рдХреЗ рд╕рд╛рде рд╕рдВрдХрд▓рд┐рдд рдХрд┐рдпрд╛ рдЧрдпрд╛ рд╣реИред
-v coqchk рд╕рдВрд╕реНрдХрд░рдг рдкреНрд░рд┐рдВрдЯ рдХрд░реЗрдВ рдФрд░ рдмрд╛рд╣рд░ рдирд┐рдХрд▓реЗрдВред
-coqlib рджреАрд░
рдорд╛рдирдХ рд▓рд╛рдЗрдмреНрд░реЗрд░реА рдХреЗ рдбрд┐рдлрд╝реЙрд▓реНрдЯ рд╕реНрдерд╛рди рдХреЛ рдУрд╡рд░рд░рд╛рдЗрдб рдХрд░рддрд╛ рд╣реИред
-рдХрд╣рд╛рдВ рд╣реИ coqchk рдорд╛рдирдХ рд▓рд╛рдЗрдмреНрд░реЗрд░реА рд╕реНрдерд╛рди рдФрд░ рдирд┐рдХрд╛рд╕ рдкреНрд░рд┐рдВрдЯ рдХрд░реЗрдВред
-рдПрдЪ, --рдорджрдж
рд╡рд┐рдХрд▓реНрдкреЛрдВ рдХреА рд╕реВрдЪреА рдкреНрд░рд┐рдВрдЯ рдХрд░реЗрдВ
onworks.net рд╕реЗрд╡рд╛рдУрдВ рдХрд╛ рдЙрдкрдпреЛрдЧ рдХрд░рдХреЗ рдСрдирд▓рд╛рдЗрди coqchk.opt рдХрд╛ рдЙрдкрдпреЛрдЧ рдХрд░реЗрдВ