From a47b49b11d17add5ca1ea5e650d2f344219b4f7e Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 5 Feb 2016 15:24:42 -0500 Subject: Update build process to use COQPATH & _CoqProject Removed all of the files not built by default; they can be resurrected from git history. _CoqProject is the standard way to list the files in a project and to give information to coq_makefile. COQPATH is the standard way to make use of not-yet-installed libraries that are not part of your project (i.e., you don't want to remove them when you `make clean`, etc.). --- coqprime/gencertif/pocklington.c | 277 --------------------------------------- 1 file changed, 277 deletions(-) delete mode 100644 coqprime/gencertif/pocklington.c (limited to 'coqprime/gencertif/pocklington.c') diff --git a/coqprime/gencertif/pocklington.c b/coqprime/gencertif/pocklington.c deleted file mode 100644 index 89b2029ff..000000000 --- a/coqprime/gencertif/pocklington.c +++ /dev/null @@ -1,277 +0,0 @@ -/* -(*************************************************************) -(* This file is distributed under the terms of the *) -(* GNU Lesser General Public License Version 2.1 *) -(*************************************************************) -(* Benjamin.Gregoire@inria.fr Laurent.Thery@inria.fr *) -(*************************************************************) -*/ - -#include -#include -#include -#include -#include "gmp.h" -#include "ecm.h" -#include "certif.h" -#include "factorize.h" - - -#if defined (__STDC__) \ - || defined (__cplusplus) \ - || defined (_AIX) \ - || defined (__DECC) \ - || (defined (__mips) && defined (_SYSTYPE_SVR4)) \ - || defined (_MSC_VER) \ - || defined (_WIN32) -#define __ECM_HAVE_TOKEN_PASTE 1 -#else -#define __ECM_HAVE_TOKEN_PASTE 0 -#endif - -#ifndef __ECM -#if __ECM_HAVE_TOKEN_PASTE -#define __ECM(x) __ecm_##x -#else -#define __ECM(x) __ecm_/**/x -#endif -#endif - -#define pp1_random_seed __ECM(pp1_random_seed) -void pp1_random_seed (mpz_t, mpz_t, gmp_randstate_t); -#define pm1_random_seed __ECM(pm1_random_seed) -void pm1_random_seed (mpz_t, mpz_t, gmp_randstate_t); -#define get_random_ul __ECM(get_random_ul) -unsigned long get_random_ul (void); - -void usage () -{ - fprintf(stdout,"usage ; pocklington [-v] [-o file] [-n name] numspec\n"); - fprintf(stdout,"numspec = prime | -next number\n"); - fprintf(stdout," = -size number | -proth k n | -lucas number \n"); - fprintf(stdout," | -mersenne number | -dec filename\n"); - fflush(stdout); - exit (-1); -} - -int -main (int argc, char *argv[]) -{ - mpz_t t; - pre_certif_t p; - pock_certif_t c; - certif_t lc; - char *filename; - int defaultname = 1; - char *lemmaname; - lemmaname = "myPrime"; - c = NULL; - - if (argc < 2) { - usage(); - } - - while (1) { - - if (!strcmp (argv[1], "-v")) { - my_set_verbose(); - argv++; - argc--; - } else if (!strcmp (argv[1], "-o")) { - if (argc == 2) usage(); - filename = argv[2]; - defaultname = 0; - argv += 2; - argc -= 2; - } else if (!strcmp (argv[1], "-n")) { - if (argc == 2) usage(); - lemmaname = argv[2]; - argv += 2; - argc -= 2; - } else - -break; - } - - mpz_init (t); - lc = init_certif(); - - switch (argc) { - case 2: - mpz_set_str (t, argv[1], 0); - if (!mpz_probab_prime_p (t, 3)) { - mpz_out_str (stdout, 10, t); - fprintf(stdout," is not a prime number\n"); - fflush(stdout); - exit (-1); - } - c = pock_certif(t); - break; - - case 3: - if (!strcmp(argv[1], "-size")) - { - unsigned long int size; - gmp_randstate_t randstate; - - size = atoi(argv[2]); - gmp_randinit_default (randstate); - gmp_randseed_ui (randstate, get_random_ul ()); - mpz_urandomb (t, randstate, 4*size); - while ( mpz_sizeinbase(t,10) <= size) - mpz_urandomb (t, randstate, 4*size); - - while (mpz_sizeinbase(t,10) > size) mpz_tdiv_q_2exp(t,t,1); - - mpz_nextprime (t, t); - c = pock_certif(t); - break; - } - - if (!strcmp (argv[1], "-next")) - { - mpz_set_str (t, argv[2], 0); - mpz_nextprime (t, t); - c = pock_certif(t); - break; - } - - if (!strcmp(argv[1], "-lucas")) - { - unsigned long int n; - n = atoi(argv[2]); - /* compute the mersenne number */ - mpz_set_ui(t, 1);mpz_mul_2exp(t, t, n);mpz_sub_ui(t, t, 1); - fprintf(stdout,"mersenne %lu = ", n); - mpz_out_str (stdout, 10, t); - fprintf(stdout, "\n"); - /* Check primality */ - if (!mpz_probab_prime_p (t, 3)) { - fprintf(stdout,"is not a prime number\n"); fflush(stdout); - exit (-1); - } - /* build the filename */ - if (defaultname) - { - int size; - size = /*mersenne.v*/ 7 + strlen (argv[2])+1; - filename = (char *)malloc(size); - strcpy(filename,"lucas"); - strcat(filename,argv[2]); - strncat(filename,".v",2); - defaultname = 0; - } - p = mk_lucas_certif(t, n); - break; - } - - if (!strcmp(argv[1], "-mersenne")) - { - unsigned long int n; - n = atoi(argv[2]); - /* compute the mersenne number */ - mpz_set_ui(t, 1);mpz_mul_2exp(t, t, n);mpz_sub_ui(t, t, 1); - fprintf(stdout,"mersenne %lu = ", n); - mpz_out_str (stdout, 10, t); - fprintf(stdout, "\n"); - /* Check primality */ - if (!mpz_probab_prime_p (t, 3)) { - fprintf(stdout,"is not a prime number\n"); fflush(stdout); - exit (-1); - } - /* build the filename */ - if (defaultname) - { - int size; - size = /*mersenne.v*/ 10 + strlen (argv[2])+1; - filename = (char *)malloc(size); - strcpy(filename,"mersenne"); - strcat(filename,argv[2]); - strncat(filename,".v",2); - defaultname = 0; - } - c = mersenne_certif(t, n); - break; - } - - if (!strcmp(argv[1], "-dec")) - { - c = read_file(argv[2], lc); - - if (defaultname) - { - int size; - size = strlen (argv[2])+3; - filename = (char *)malloc(size); - strcpy(filename,argv[2]); - strncat(filename,".v",2); - defaultname = 0; - } - fprintf(stdout, "build certificate for\n"); - mpz_out_str (stdout, 10, c->_N); - fprintf(stdout, "\n"); fflush(stdout); - finalize_pock(c); - p = mk_pock_certif(c); - break; - } - else usage(); - - case 4: - if (!strcmp(argv[1], "-proth")) - { - unsigned long int n, k; - k = atoi(argv[2]); - n = atoi(argv[3]); - mpz_set_ui (t, k); - mpz_mul_2exp (t, t, n); - mpz_add_ui (t, t, 1); - if (!mpz_probab_prime_p (t, 3)) { - mpz_out_str (stdout, 10, t); - fprintf(stdout," is not a prime number\n"); - fflush(stdout); - exit (-1); - } - c = pock_certif(t); - break; - } - - default: - usage(); - } - - if (defaultname) { - int size, len; - int filedes[2]; - FILE *fnin; - FILE *fnout; - filename = "Prime.v"; - pipe(filedes); - fnout = fdopen(filedes[1],"w"); - fnin = fdopen(filedes[0], "r"); - fprintf(fnout,"prime"); - size = 5; - len = mpz_out_str (fnout, 10, t); - size += len; - fprintf(fnout,".v"); fflush(fnout); - size += 2; - if (size > FILENAME_MAX-1) filename = "Prime.v"; - else { - filename = (char *)malloc(size+1); - fread(filename, 1, size, fnin); - filename[size] = '\0'; - } - fclose(fnin); - fclose(fnout); - } - - if (c != NULL) { - p = mk_pock_certif(c); - extend_lc (lc, c, 0, 0); - } - - print_file(filename, lemmaname, p, lc); - - fprintf(stdout,"\n");fflush(stdout); - mpz_clear(t); - exit (0); -} -- cgit v1.2.3