Provided by: coqprime-tools_8.17-1build1_amd64
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)