diff --git a/resources/templates/spark_main/example.yaml b/resources/templates/spark_main/example.yaml
index 5cc4d4d..ed6ae72 100644
--- a/resources/templates/spark_main/example.yaml
+++ b/resources/templates/spark_main/example.yaml
@@ -1,3 +1,2 @@
 name: SPARK Main
 description: Simple overrideable provable main
-main: main
diff --git a/resources/templates/spark_main/gnatprove/abdasd.adb.stderr b/resources/templates/spark_main/gnatprove/abdasd.adb.stderr
new file mode 100644
index 0000000..09b0a52
--- /dev/null
+++ b/resources/templates/spark_main/gnatprove/abdasd.adb.stderr
@@ -0,0 +1 @@
+abdasd.adb:1:01: compilation unit expected
diff --git a/resources/templates/spark_main/gnatprove/abdasd.adb.stdout b/resources/templates/spark_main/gnatprove/abdasd.adb.stdout
new file mode 100644
index 0000000..e69de29
diff --git a/resources/templates/spark_main/gnatprove/gnatprove.out b/resources/templates/spark_main/gnatprove/gnatprove.out
new file mode 100644
index 0000000..8b13789
--- /dev/null
+++ b/resources/templates/spark_main/gnatprove/gnatprove.out
@@ -0,0 +1 @@
+
diff --git a/resources/templates/spark_main/gnatprove/why3.conf b/resources/templates/spark_main/gnatprove/why3.conf
new file mode 100644
index 0000000..b3c4b2b
--- /dev/null
+++ b/resources/templates/spark_main/gnatprove/why3.conf
@@ -0,0 +1,71 @@
+[main]
+magic =  14
+memlimit =  0
+[editor coqide]
+name = "CoqIDE"
+command = "coqide -I %l/coq-tactic -R %o/why3_libs/coq Why3 %f"
+[prover]
+command = "alt-ergo -max-split 5 %f"
+command_steps = "alt-ergo -steps-bound %S -max-split 5 %f"
+driver = "alt-ergo_gnatprove.drv"
+name = "altergo"
+shortcut = "altergo"
+version = "1.30-gnatprove"
+[prover]
+command = "cvc4 --lang=smt2 --stats --no-cond-rewrite-quant --bitblast-step=5 --cnf-step=5 --lemma-step=5 --parse-step=0 --preprocess-step=0 --restart-step=10 --rewrite-step=0 %f"
+command_steps = "cvc4 --rlimit=%S --lang=smt2 --stats --no-cond-rewrite-quant --bitblast-step=5 --cnf-step=5 --lemma-step=5 --parse-step=0 --preprocess-step=0 --restart-step=10 --rewrite-step=0 %f"
+driver = "cvc4_gnatprove.drv"
+name = "CVC4"
+shortcut = "cvc4"
+version = "1.6-gnatprove"
+[prover]
+command = "cvc4 --lang=smt2 --stats --no-cond-rewrite-quant --bitblast-step=5 --cnf-step=5 --lemma-step=5 --parse-step=0 --preprocess-step=0 --restart-step=10 --rewrite-step=0 %f"
+command_steps = "cvc4 --rlimit=%S --lang=smt2 --stats --no-cond-rewrite-quant --bitblast-step=5 --cnf-step=5 --lemma-step=5 --parse-step=0 --preprocess-step=0 --restart-step=10 --rewrite-step=0 %f"
+driver = "cvc4_gnatprove_extra_axioms.drv"
+name = "CVC4_More_Axioms"
+shortcut = "cvc4_axioms"
+version = "1.6-gnatprove"
+[prover]
+command = "cvc4 --lang=smt2 --stats --bitblast-step=5 --cnf-step=5 --lemma-step=5 --parse-step=0 --preprocess-step=0 --restart-step=10 --rewrite-step=0 %f"
+command_steps = "cvc4 --rlimit=%S --lang=smt2 --stats --bitblast-step=5 --cnf-step=5 --lemma-step=5 --parse-step=0 --preprocess-step=0 --restart-step=10 --rewrite-step=0 %f"
+driver = "cvc4_gnatprove_qf.drv"
+name = "CVC4_QF"
+shortcut = "cvc4_qf"
+version = "1.6-gnatprove"
+[prover]
+command = "cvc4 --tlimit-per=%t000 --lang=smt2 --stats --no-cond-rewrite-quant --bitblast-step=5 --cnf-step=5 --lemma-step=5 --parse-step=0 --preprocess-step=0 --restart-step=10 --rewrite-step=0 --macros-quant --quiet %f"
+command_steps = "cvc4 --rlimit=%S --lang=smt2 --stats --no-cond-rewrite-quant --bitblast-step=5 --cnf-step=5 --lemma-step=5 --parse-step=0 --preprocess-step=0 --restart-step=10 --rewrite-step=0 --macros-quant --quiet %f"
+driver = "cvc4_gnatprove_ce.drv"
+name = "CVC4_CE"
+shortcut = "cvc4_ce"
+version = "1.6-gnatprove"
+[prover]
+command = "z3 -smt2 -st %f"
+command_steps = "z3 rlimit=%S -smt2 -st %f"
+driver = "z3_gnatprove.drv"
+name = "Z3"
+shortcut = "z3"
+version = "4.5.1-gnatprove"
+[prover]
+command = "z3 -smt2 -st %f"
+command_steps = "z3 rlimit=%S -smt2 -st %f"
+driver = "z3_no_quant.drv"
+name = "Z3_noquant"
+shortcut = "z3_noquant"
+version = "4.5.1-gnatprove"
+[prover]
+command = "z3 -t:%t -smt2 -st %f"
+command_steps = "z3 rlimit=%S -smt2 -st %f"
+driver = "z3_gnatprove_ce.drv"
+name = "z3_ce"
+shortcut = "z3_ce"
+version = "4.5.1-gnatprove"
+[prover]
+command = "coqtop -batch -I %l/coq-tactic -R %o/why3_libs/coq Why3 -l %f"
+driver = "coq_gnatprove.drv"
+name = "Coq"
+shortcut = "coq"
+version = "8.5pl2"
+interactive = true
+editor = "coqide"
+in_place = false
diff --git a/resources/templates/spark_main/main.adb b/resources/templates/spark_main/main.adb
deleted file mode 100644
index e0d8401..0000000
--- a/resources/templates/spark_main/main.adb
+++ /dev/null
@@ -1,4 +0,0 @@
-procedure Main is
-begin
-   null;
-end Main;
diff --git a/resources/templates/spark_main/main.adc b/resources/templates/spark_main/main.adc
index 6a07ed7..a6f5657 100644
--- a/resources/templates/spark_main/main.adc
+++ b/resources/templates/spark_main/main.adc
@@ -4,3 +4,4 @@ pragma Partition_Elaboration_Policy(Sequential);
 pragma SPARK_Mode (On);
 pragma Warnings (Off, "no Global contract available");
 pragma Warnings (Off, "subprogram * has no effect");
+pragma Warnings (Off, "file name does not match");
diff --git a/resources/templates/spark_main/main.gpr b/resources/templates/spark_main/main.gpr
index 7e52d62..739d795 100644
--- a/resources/templates/spark_main/main.gpr
+++ b/resources/templates/spark_main/main.gpr
@@ -1,9 +1,7 @@
 project Main is
 
-   for Main use ("main.adb");
-
    package Compiler is
-      for Switches ("ada") use ("-g", "-gnatwa", "-gnatQ");
+      for Switches ("ada") use ("-g");
    end Compiler;
 
    package Builder is