Provided by: coqprime-tools_8.15-1_amd64 bug

NAME

       pocklington - generate a Pocklington primality certificate for a prime number

SYNOPSIS

       pocklington [-o filename] prime
       pocklington [-o filename] -next num
       pocklington [-o filename] -size s
       pocklington [-o filename] -proth k n
       pocklington [-o filename] -lucas n
       pocklington [-o filename] -mersenne n
       pocklington [-o filename] -dec filename

DESCRIPTION

       This  tool  takes  a  prime  number  and  (tries  to)  generate  a  Pocklington  primality
       certificate.

OPTIONS

       -v Enable verbose mode -o <filename> Prints the proof script in the file named  <filename>
       (otherwise the name depends on the way the prime was given)

       <prime>
              A  prime  number.  The default output filename is either prime<prime>.v or, if it's
              too long, Prime.v

       -next <num>
              Generate a certificate for the next  prime  number  following  <num>.  The  default
              output filename is as if the right number had been given.

       -size <s>
              Generate  a  certificate  for  a prime number with at least <s> decimal digits. The
              default output filename is as if the right number had been given.

       -proth <k> <n>
              Generate a certificate for the Proth number k*2^n+1. The default output filename is
              as if the right number had been given.

       -lucas <n>
              Generate  a  certificate  for  the  Mersenne  number  2^n-1 using Lucas' test (more
              efficient). The default output filename is lucas<n>.v.

       -mersenne <n>
              Generate a certificate for the Mersenne number 2^n-1 using Pocklington's test.  The
              default output filename is mersenne<n>.v.

       -dec <filename>
              Generate  a  certificate  for  the  number  given in the file <filename> ; the file
              should also contain a partial factorization of the predecessor. The output filename
              is <filename>.v.

                                         July 15th, 2022                           POCKLINGTON(1)