what is the `configure` command e.g. when building CompCert? Are there other unexpected commands like that needed during the compiling process of each coq proj?

brando90 commented 1 year ago

I saw:

       "build_command": "configure x86_64-linux && make"

how do I run that? I get:

(iit_synthesis) brando9/afs/cs.stanford.edu/u/brando9/proverbot9001/CompCert $ configure x86_64-linux
configure: command not found

I don't have pseudo privileges & scared of installing such a command...how do I install it?

brando90 commented 1 year ago

I did:

cd /afs/cs.stanford.edu/u/brando9/proverbot9001/CompCert/
configure x86_64-linux
make .

brando90 commented 1 year ago

hmmm do I just souce the make.sh file? but you have a make command:

(iit_synthesis) brando9/afs/cs.stanford.edu/u/brando9/proverbot9001/CompCert $ make .
Makefile:16: Makefile.config: No such file or directory
make: *** No rule to make target 'Makefile.config'.  Stop.
(iit_synthesis) brando9/afs/cs.stanford.edu/u/brando9/proverbot9001/CompCert $ ls
aarch64  cfrontend  configure  debug   exportclight  lib       Makefile.extr    MenhirLib  README.md  test     x86
arm  Changelog  coq        doc     extraction    LICENSE   Makefile.menhir  pg     riscV      tools    x86_32
backend  common     cparser    driver  flocq         Makefile  make.sh      powerpc    runtime    VERSION  x86_64

brando90 commented 1 year ago

this is the split.json file, doesn't seem to work? I think the build command is source make.sh

[
    {
        "project_name": "CompCert",
        "train_files": [
            "cfrontend/Cshmgen.v",
            "cfrontend/Initializersproof.v",
            "cfrontend/Csharpminor.v",
            "cfrontend/Cstrategy.v",
            "cfrontend/SimplLocalsproof.v",
            "cfrontend/SimplExpr.v",
            "cfrontend/Cexec.v",
            "cfrontend/SimplExprspec.v",
            "cfrontend/Initializers.v",
            "cfrontend/Ctyping.v",
            "cfrontend/Cminorgenproof.v",
            "cfrontend/Csem.v",
            "cfrontend/SimplExprproof.v",
            "cfrontend/Cshmgenproof.v",
            "cfrontend/ClightBigstep.v",
            "cfrontend/Ctypes.v",
            "cfrontend/SimplLocals.v",
            "cfrontend/Csyntax.v",
            "cfrontend/Clight.v",
            "cfrontend/Cminorgen.v",
            "MenhirLib/Automaton.v",
            "MenhirLib/Validator_classes.v",
            "MenhirLib/Interpreter_correct.v",
            "MenhirLib/Alphabet.v",
            "MenhirLib/Interpreter.v",
            "MenhirLib/Main.v",
            "MenhirLib/Grammar.v",
            "MenhirLib/Validator_safe.v",
            "MenhirLib/Interpreter_complete.v",
            "x86_64/Archi.v",
            "cparser/Cabs.v",
            "flocq/Prop/Plus_error.v",
            "flocq/Prop/Round_odd.v",
            "flocq/Prop/Div_sqrt_error.v",
            "flocq/Prop/Double_rounding.v",
            "flocq/Prop/Relative.v",
            "flocq/Prop/Sterbenz.v",
            "flocq/Calc/Operations.v",
            "flocq/Calc/Bracket.v",
            "flocq/Calc/Sqrt.v",
            "flocq/Calc/Div.v",
            "flocq/IEEE754/Binary.v",
            "flocq/IEEE754/Bits.v",
            "flocq/Core/FTZ.v",
            "flocq/Core/FLX.v",
            "flocq/Core/Generic_fmt.v",
            "flocq/Core/Core.v",
            "flocq/Core/Digits.v",
            "flocq/Core/Round_pred.v",
            "flocq/Core/Round_NE.v",
            "flocq/Core/FIX.v",
            "flocq/Core/FLT.v",
            "flocq/Core/Raux.v",
            "flocq/Core/Float_prop.v",
            "flocq/Core/Defs.v",
            "flocq/Core/Ulp.v",
            "x86/Conventions1.v",
            "x86/CombineOp.v",
            "x86/ConstpropOp.v",
            "x86/ConstpropOpproof.v",
            "x86/Asmgen.v",
            "x86/NeedOp.v",
            "x86/ValueAOp.v",
            "x86/Builtins1.v",
            "x86/Machregs.v",
            "x86/Asmgenproof1.v",
            "x86/SelectOp.v",
            "x86/SelectLongproof.v",
            "x86/CombineOpproof.v",
            "x86/Op.v",
            "x86/SelectLong.v",
            "x86/Asmgenproof.v",
            "x86/Stacklayout.v",
            "x86/Asm.v",
            "backend/Mach.v",
            "backend/Constprop.v",
            "backend/RTLgen.v",
            "backend/RTLgenproof.v",
            "backend/ValueDomain.v",
            "backend/RTLgenspec.v",
            "backend/Renumber.v",
            "backend/Tunnelingproof.v",
            "backend/Linear.v",
            "backend/Liveness.v",
            "backend/Inliningspec.v",
            "backend/SplitLongproof.v",
            "backend/Stacking.v",
            "backend/Debugvarproof.v",
            "backend/CSE.v",
            "backend/Asmgenproof0.v",
            "backend/Allocation.v",
            "backend/Selection.v",
            "backend/Renumberproof.v",
            "backend/Conventions.v",
            "backend/LTL.v",
            "backend/Inlining.v",
            "backend/Linearizeproof.v",
            "backend/Linearize.v",
            "backend/Stackingproof.v",
            "backend/SplitLong.v",
            "backend/Deadcodeproof.v",
            "backend/Tailcall.v",
            "backend/CSEproof.v",
            "backend/ValueAnalysis.v",
            "backend/Registers.v",
            "backend/Unusedglob.v",
            "backend/Lineartyping.v",
            "backend/Tunneling.v",
            "backend/Unusedglobproof.v",
            "backend/SelectDivproof.v",
            "backend/Deadcode.v",
            "backend/CleanupLabels.v",
            "backend/Cminortyping.v",
            "backend/CleanupLabelsproof.v",
            "backend/SelectDiv.v",
            "backend/Tailcallproof.v",
            "backend/Allocproof.v",
            "backend/Constpropproof.v",
            "backend/CminorSel.v",
            "backend/NeedDomain.v",
            "backend/Kildall.v",
            "backend/RTLtyping.v",
            "backend/Bounds.v",
            "backend/Cminor.v",
            "backend/Inliningproof.v",
            "backend/CSEdomain.v",
            "backend/Debugvar.v",
            "common/Events.v",
            "common/Behaviors.v",
            "common/Memory.v",
            "common/Values.v",
            "common/Builtins0.v",
            "common/Smallstep.v",
            "common/Memtype.v",
            "common/Switch.v",
            "common/Linking.v",
            "common/Unityping.v",
            "common/Separation.v",
            "common/Memdata.v",
            "common/Determinism.v",
            "common/Builtins.v",
            "common/AST.v",
            "common/Errors.v",
            "driver/Complements.v",
            "driver/Compopts.v",
            "driver/Compiler.v",
            "lib/Zbits.v",
            "lib/Ordered.v",
            "lib/Lattice.v",
            "lib/IEEE754_extra.v",
            "lib/Coqlib.v",
            "lib/FSetAVLplus.v",
            "lib/IntvSets.v",
            "lib/BoolEqual.v",
            "lib/Iteration.v",
            "lib/Floats.v",
            "lib/UnionFind.v",
            "lib/Decidableplus.v",
            "lib/Integers.v",
            "lib/Heaps.v",
            "lib/Maps.v",
            "lib/Postorder.v",
            "lib/Axioms.v",
            "lib/Intv.v"
        ],
        "test_files": [
            "backend/Locations.v",
            "backend/RTL.v",
            "backend/Selectionproof.v",
            "cfrontend/Cop.v",
            "exportclight/Clightdefs.v",
            "MenhirLib/Validator_complete.v",
            "x86/SelectOpproof.v",
            "flocq/Calc/Round.v",
            "flocq/Prop/Mult_error.v",
            "flocq/Core/Zaux.v",
            "lib/Parmov.v",
            "lib/Wfsimpl.v",
            "common/Globalenvs.v"
        ],
        "switch": "coq-8.10",
        "build_command": "configure x86_64-linux && make"
    }
]

HazardousPeach commented 1 year ago

Uhh, I think you're running on an old commit or something? In both the develop and master branches that line looks different now: https://github.com/UCSD-PL/proverbot9001/blob/e89e89cf3b3ee24d04b2dc5e965e787f714340f0/coqgym_projs_splits.json#L2227 https://github.com/UCSD-PL/proverbot9001/blob/8a63ed4dac3fc40917d005db51dc8e8856aca8a6/coqgym_projs_splits.json#L2227 It should be ./configure x86_64-linux && make, not configure x86_64-linux && make. The former is calling the local configure script within the directory, which generates the makefile. So you shouldn't need to install any other commands. make.sh is a local file generated by some of my build scripts for a cluster, which basically just does the cluster permissions workaround, runs eval $(opam env), and then runs the build commands in the json. If you're not running on a cluster, you can just run the build commands.

brando90 commented 1 year ago

@HazardousPeach do I really need the configure command in the build the /configure x86_64-linux?

brando90 commented 1 year ago

If you're not running on a cluster, you can just run the build commands.

Great

brando90 commented 1 year ago

then runs the build commands in the json. If you're not running on a cluster, you can just run the build commands.

not quite, you still need to set the switch correctly before the make e.g.

    SWITCH=$(jq -r ".[] | select(.project_name == \"$project\") | .switch" coqgym_projs_splits.json)

    # todo: why not just call opam switch? or `opam switch set {$SWITCH}`
    echo "eval \"$(opam env --set-switch --switch=$SWITCH)\"" >> coq-projects/$project/make.sh

but above doesn't work in python so you need to do:

    command: str = f'opam switch set {switch}'
    logging.info(f"-> {command=}")
    try:
        res = subprocess.run(command.split(), check=True, stdout=subprocess.PIPE, stderr=subprocess.PIPE)
        # res = subprocess.run(command, check=True, stdout=subprocess.PIPE, stderr=subprocess.PIPE)
        logging.info(f'{res.stdout.decode=}')
        logging.info(f'{res.stderr.decode=}')
    except Exception as e:
        logging.critical(f'Error: {e=}')
        raise e

in my experience.

HazardousPeach commented 1 year ago

@HazardousPeach do I really need the configure command in the build the /configure x86_64-linux?

Yes, without the configure command there is no Makefile to build from. If you see a makefile, someone must have already run ./configure. The makefile also changes depending on which target architecture you pass to configure.

not quite, you still need to set the switch correctly before the make e.g.

Ah right, you do need to set the switch before you can build, I sort of assumed that you would do that once in your shell before doing anything else, but since they need separate shells yeah. If you're using coq_serapy (which is a dependency of proverbot9001), you can just run coq_serapy.set_switch("<switch-name>") in python to set the switch. Otherwise you might still need to run eval $(opam env) in a shell before building, because opam wants to set some environment variables.

UCSD-PL / proverbot9001

what is the `configure` command e.g. when building CompCert? Are there other unexpected commands like that needed during the compiling process of each coq proj? #65